12,080
edits
Changes
Directory:Jon Awbrey/Papers/Inquiry Driven Systems : Part 6 (view source)
Revision as of 03:54, 24 February 2013
, 03:54, 24 February 2013→6.37. Propositional Types: markup
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.
<pre>
<pre>
Definition. A relation R c XxY has type S.T, written R : S.T, iff every <x, y> C R has type S.T, that is, iff R c SxT for some S c X and T c Y.
Definition. A relation R c XxY has type S.T, written R : S.T, iff every <x, y> C R has type S.T, that is, iff R c SxT for some S c X and T c Y.