Types

Types are structured collections of objects such as natural numbers, ${{\mathbb{N} }}$, or pairs of numbers ${{\mathbb{N} }} \times {{\mathbb{N} }}$ or lists of numbers, etc. In the section on type theory we will present specific concrete types, here we treat the notion abstractly. We think of the elements of the types as possibly given first without specifying the type; they might be built from sets for example or be the raw data in a computer (the bytes) or be physical objects or be given by constructions. Even when we are thinking of constructing objects according to a method specified by the type (as for the natural numbers based on zero and successor), still we imagine the object as existing without type information attached to it, and thus objects can be in more than one type.

The critical point about judging that T is a type is knowing what it means for an expression to be an element of T. This is what we know when we show that T is a type.

Assertions about objects require their classification into types. Moreover, we need relative or hypothetical classification because an object t occurring in a proposition may be built contingently from other objects x_i of type T_i, and will be in some type T. We understand these relative type membership judgments as follows. To judge that t[x] is a member of T₂ provided xis a member of T₁ means that for any object t₁ of type T₁, t[t₁] is an object of T₂. We write this as $x\!:\!T_1 \vdash t[x] \in T_2$. We extend the notation to n assumptions by writing $x_1\!:\!T_1, \ldots, x_n\!:\!T_n \vdash t \in T$ for x_i distinct identifiers. (We write $t[x_1, \ldots, x_n]$ only when we need to be explicit about the variables; this notation is a second order variable.) We give concrete examples of this judgment below and discuss them at length in section 3.

We don't treat this judgment as an assertion. It summarizes what must hold for a statement about t to make sense. It is not the kind of expression that is true or false. For example, when we say $0 \in {{\mathbb{N} }}$, we are thinking that 0 is a natural number. This is a fact. We are thinking `` $0\, is\_a\, {{\mathbb{N} }}$,'' and it does not make sense to deny this, thinking that 0is something else.

In order to consider propositional functions of more than one argument, say P(x, y), we explicitly construct pairs of elements, $\langle x, y\rangle$ and express P(x, y) as $P(\langle x, y\rangle)$. The pair $\langle x, y\rangle$belongs to the Cartesian product type. So our types have at least this structure.

Definition 1   ordered paircartesian product If A, B are types, then so is their Cartesian product, $A \times B$. If $a \in A$ and $b \in B$ then the ordered pair $\langle a, b\rangle$ belongs to $A \times B$. We write $\langle a, b\rangle \in A \times B$. We write $1o\!f\left(\left\langle a, b\right\rangle\right) = a$ and $2o\!f\left(\left\langle a, b\right\rangle\right) = b$. Let Aⁿ denote $A\times\cdots \times A$ taken n times.

Propositions are elements of the large type (or category) Prop. We use membership judgements

$$x_1 : T_1, \ldots, x_n : T_n \vdash P \in Prop$$

or an abbreviation ${\cal{T}} \vdash P \in Prop$ to define them. Atomic propositions are constants: $\top$ for a canonically true canonically true proposition one and $\perp$ for a canonically false canonically false proposition one, or propositional variables or applications of propositional function variables in the large type $(T \rightarrow Prop)$ for some type T. Compound propositionscompound proposition are built from the logical connectives &, $\vee, \Rightarrow$ or the logical operators $\exists$ and $\forall$.

The membership rules are that if ${\cal{T}} \vdash F \in Prop$ and ${\cal{T}} \vdash G \in Prop$, then ${\cal{T}} \vdash (F \; op \; G)\in Prop$ for opa connective; and if $x_1 : T_1, \ldots,x_n : T_n \vdash F \in Prop$, then ${\cal{T}^\prime} \vdash (Q x_i : T_i\, . \, F) \in Prop$ where Q is a quantification operator and where $\cal{T}^\prime$is obtained by removing the typing assumption $x_i \, : \, T_i$.

The usual names for the compound propositions are:

proposition		English equivalent	operator name
$(F\: \&\: G)$	is	F and G	conjunction
$(F \vee G)$	is	F or G	disjunction
$(F \Rightarrow G)$	is	F implies G	implication
F(t)	is	F at t	instance
$\forall x\!:\!A. F(x)$	is	for all x of type A, F(x)	universal quantification
$\exists x\!:\!A. F(x)$	is	for some x of type A, F(x)	existential quantification

With these definitions in place we can write examples of general typed propositions. We use definiendum == definiens to write definitions.

Definition 2   For any propositions F and G define

$$\begin{eqnarray*}\neg\: F & =\, = & (F \Rightarrow \perp) \\ (F \Leftarrow G) &... ...tarrow G) & =\, = & ((F \Leftarrow G)\: \&\: (F \Rightarrow G)). \end{eqnarray*}$$

For $P : ((A \times B) \rightarrow\ Prop)$let $P(x, y) =\, = P(\langle x, y\rangle).$