Typed logic

Ordinary mathematical statements are usually expressed in a typed languagetype. Consider the trivially true proposition: ``if there is a rational number q whose absolute value is less than the reciprocal of any natural number n, then for every natural number n, there is a real number r whose absolute value is also less than 1/n.'' Symbolically we express this as follows for ${{\mathbb{N} }}$ the natural numbers, ${{\mathbb{Q} }}$ the rationals, and ${{\mathbb{R} }}$ the reals:

$$*\ \ \ \ \ \ \exists q\!:\! {{\mathbb{Q} }}.\ \forall n\!:\! ... ...sts r\!:\! {{\mathbb{R} }}.\ \left(\vert r\vert < 1/n\right).$$

We can abstract on the relation |r| < 1/n, and speak of any relation L on ${{\mathbb{N} }} \times {{\mathbb{R} }}$ and recognize that ${{\mathbb{Q} }}$ is a subtypesubtype of ${{\mathbb{R} }}$ to obtain

$$\exists q\!:\! {{\mathbb{Q} }}.\ \forall n\!:\!{{\mathbb{N} }... ...b{N} }}.\ \exists r\!:\!{{\mathbb{R} }}.\ L\left(n, r\right).$$

Abstracting further, we know that for any types A, A' and B where A' is a subtypesubtype of A, say $A'\sqsubseteq A$ the following is true

$$\exists a\!:\!A'.\ \forall x\!:\!B.\ L(x, a) \Rightarrow \forall x\!:\!B.\ \exists a\!:\!A.\ L\left(a, x\right).$$

This last statement is an abstraction of * with respect to ${{\mathbb{Q} }}, {{\mathbb{N} }},{{\mathbb{R} }}$ and the relation |r| < 1/n. It is these purely abstract typed propositions that we want to study in the beginning. We want to know what statements are true regardless of the types and the exact propositions. We are looking for those properties of mathematical propositions that are invariant under arbitrary replacement of types and propositions.

Here logic is presented in a way that relates it closely to the type theory of section 3 and the programming language of section . Essentially, we will be able to lay one presentation on top of the others and see a striking correspondence as Table 1 suggests. This goal leads to a novel presentation of logic because of the role of explicit typing judgments. We begin now to gradually make these ideas more precise.