Also see Standard Correspondence between Propositions and Types for newer supplementary material.
The first example of a logic that we express in type theory is constructive logic. This logic is very close in spirit to the constructive principles underlying type theory, so expressing constructive logic amounts to interpreting the type constructors of the Nuprl logic as logical connectives using the informal semantics of evidence that was employed in the discussion of propositions as types.
The definitions in figure express the correspondence between logical connectives and type constructors.
We treat as , so we do not need an explicit definition for the usual logical ``or'' in terms of the type constructors. We could also include notations all3, some3, all4, etc., for higher numbers of variables of the same type, but in practice two or three suffice most of the time.
The rules for the logical operators defined in this way are exactly the rules for constructive logic; see for example [Dummet 77]. We will discuss this at length in chapter 4 when we study proofs and rules; however, one can see the intentions behind these definitions in terms of an informal semantics of evidence of the kind mentioned in chapter 1. Consider first the definition and; there is evidence for A & B precisely when there is a pair, , such that a is evidence for A and b is evidence for B. Thus treating A & B as A # B is semantically correct from this viewpoint.
Consider next. According to the constructive interpretation, is true when we have evidence for A or for B and when we can tell from the evidence which of A or B it supports. This is precisely the information that is available in the type . An element of the disjoint union is either or , where a is in A and b is in B and inl and inr are the canonical injections into the disjoint sum type.
Next consider . According to Brouwer [Brouwer 23], the founder of Intuitionism , an implication is true when there is a method of transforming any evidence for the antecedent, A, into evidence for the consequent, B. If A and B are represented by types, then the function space, , consists of objects which are in fact evidence for . Thus our definition is semantically correct. The definition of the biconditional, , is correct given that the definition of implication is correct.
The constructive meaning of negation is delicate. To say not A is to say that there is no evidence for A or that A will never be proved. In a type--theoretic context one way to know this is to see that there are no members in A. One might be tempted to translate not A as A = Void, but type equality means more than simply having the same members. To say A is empty, we can say A is equivalent to void, i.e., that # . However, is always inhabited, so the only new content is , which we take as our definition of not.
Figure: Constructive Logic Connectives Expressed as Types
Now consider some , which is read ``we can find an x of type A such that B is true.'' Intuitively there is evidence for an assertion of existence when we have a witness, a in A, and evidence, b, that B is true with a substituted for free variable x in B. We write this substitution as . The dependent sum type # B consists of pairs with exactly these properties, so the definition is correct.
A universal statement, all , means constructively that given any element a of A we can find evidence for . This means that there is a procedure mapping elements a of A into . This is precisely what the dependent function space provides, so this definition is also correct.
Finally, there should be no evidence for false, so the empty type, Void, is the right definition for it.
These definitions can be applied to atomic propositional forms such as the types x = y in int or x < y to produce statements such as all x:int.some y:int. x<y, which we read as ``for all integers x we can find some integer y such that x is less than y''. It is also possible to make more general statements, such as all A:U1.all x:A.x=x in A. This statement says that equality on every type is reflexive and involves quantifying over all types in ; without the hierarchy of universes it would not be possible to make such a statement predicatively.
The logical operators can be used to state general results about constructive predicate logic. Give the identification of propositions and types, which we can make more conspicuous by the definition prop == U1, we can assert theorems about constructive propositional logic. Figure gives a list of theorems that were expressed and proved in Nuprl .
Figure: Some Theorems of Constructive Propositional Logic
Statements in the predicate calculus are usually analyzed, following Frege [Frege 1879], as operators applied to propositional functions, where the term propositional function describes a function that maps objects to propositions. Given a type A, the propositional functions (of one argument) on A are of the type . With this reading some basic facts from the predicate calculus are shown in figure .
Figure: Some Predicate Calculus Theorems