Changes

This Section describes a formal system of ''type expressions'' that are analogous to formulas of propositional logic and discusses their use as a calculus of predicates for classifying, analyzing, and drawing typical inferences about <math>k\!</math>-place relations, in particular, for reasoning about the results of operations on relations and about the properties of their transformations and combinations.

This Section describes a formal system of ''type expressions'' that are analogous to formulas of propositional logic and discusses their use as a calculus of predicates for classifying, analyzing, and drawing typical inferences about <math>k\!</math>-place relations, in particular, for reasoning about the results of operations on relations and about the properties of their transformations and combinations.

'''Definition.'''  Given a cartesian product <math>X \times Y,\!</math> an ordered pair <math>(x, y) \in X \times Y,\!</math> has the type <math>S \cdot T,\!</math> written <math>(x, y) : S \cdot T,\!</math> if and only if <math>x \in S \subseteq X\!</math> and <math>y \in T \subseteq Y.\!</math>  Notice that an ordered pair may have many types.

'''Definition.'''  Given a cartesian product <math>X \times Y,\!</math> an ordered pair <math>(x, y) \in X \times Y\!</math> has the type <math>S \cdot T,\!</math> written <math>(x, y) : S \cdot T,\!</math> if and only if <math>x \in S \subseteq X\!</math> and <math>y \in T \subseteq Y.\!</math>  Notice that an ordered pair may have many types.

'''Definition.'''  A relation <math>L \subseteq X \times Y\!</math> has type <math>S \cdot T,\!</math> written <math>L : S \cdot T,\!</math> if and only if every <math>(x, y) \in L\!</math> has type <math>S \cdot T,\!</math> that is, if and only if <math>L \subseteq S \times T\!</math> for some <math>S \subseteq X\!</math> and <math>T \subseteq Y.\!</math>

'''Definition.'''  A relation <math>L \subseteq X \times Y\!</math> has type <math>S \cdot T,\!</math> written <math>L : S \cdot T,\!</math> if and only if every <math>(x, y) \in L\!</math> has type <math>S \cdot T,\!</math> that is, if and only if <math>L \subseteq S \times T\!</math> for some <math>S \subseteq X\!</math> and <math>T \subseteq Y.\!</math>