Changes

In this Section I describe a formal system of ''type expressions'' that are analogous to formulas of propositional logic, and I discuss their use as a calculus of predicates for classifying, analyzing, and drawing typical inferences about <math>n\!</math>-place relations, in particular, for reasoning about the results of operations indicated or performed on relations and about the properties of their transformations and combinations.

In this Section I describe a formal system of ''type expressions'' that are analogous to formulas of propositional logic, and I discuss their use as a calculus of predicates for classifying, analyzing, and drawing typical inferences about <math>n\!</math>-place relations, in particular, for reasoning about the results of operations indicated or performed 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 can 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.

<pre>

<pre>