Propositions as Types

An  equality form such as makes sense only if A is a type and a and b are elements of that type. How should we express the idea that is well--formed? One possibility is to use the same format as in the case of types. We could imagine a rule of the following form.

This rule expresses the right ideas, and it allows well--formedness to be treated through the proof mechanism in the same way that well--formedness is treated for types. In fact, it is clear that such an approach will be necessary for equality forms if it is necessary for types because it is essential to know that the A in is well--formed.

Thus an adequate deductive apparatus is at hand for treating the well--formedness of equalities, provided that we treat as a type. Does this make sense on other grounds as well? Can we imagine an equality as denoting a type? Or should we introduce a new category, called Prop for proposition, and prove ) in Prop? The constructive interpretation of truth of any proposition P is that P is provable. Thus it is perfectly sensible to regard a proposition P as the type of its proofs. For the case of an equality we make the simplifying assumption that we are not interested in the details of such proofs because those details do not convey any more computational information than is already contained in the equality form itself. It may be true that there are many ways to prove , and some of these may involve complex inductive arguments. However, these arguments carry only ``equality information,'' not computational information, so for simplicity we agree that equalities considered as types are either empty if they are not true or contain a single element, called axiom , if they are true.

Once we agree to treat equalities as types  (and over int, to treat a < b as a type also) then a remarkable economy in the logic is possible. For instance, we notice that the cartesian product of equalities, say , acts precisely as the conjunction  . Likewise the disjoint union, , acts exactly like the constructive disjunction.  Even more noteworthy is the fact that the dependent product, say , acts exactly like the constructive existential quantifier,  . Less obvious, but also valid, is the interpretation of as the universal statement,  .

We can think of the types built up from equalities (and inequalities in the case of integer) using , | and as propositions, for the meaning of the type constructors corresponds exactly to that of the logical operators considered constructively. As another example of this, if A and B are propositions then corresponds exactly to the constructive interpretation of .  That is, proposition A implies proposition B constructively if and only if there is a method of building a proof of B from a proof of A, which is the case if and only if there is a function f mapping proofs of A to proofs of B. However, given that A and B are types such an f exists exactly when the type is inhabited, i.e., when there is an element of type .  

It is therefore sensible to treat propositions as types. Further discussion of this principle appears in chapters 3 and 11.

Is it sensible to consider any type, say int or , as a proposition? Does it make sense to assert int? We can present the logic and the type theory in a uniform way if we agree to take the basic form of assertion as ``type A is inhabited.'' Therefore, when we write the goal we are asserting that given that the types in H are inhabited, we can build an element of A. When we want to mention the inhabiting object directly we say that it is extracted  from the proof, and we write . This means that A is inhabited by the object a.  We write the form instead of when we want to suppress the details of how A is inhabited, perhaps leaving them to be determined by a computer system as in the case of Nuprl .

When we write we are really asserting the equality

.

.

.

.