Also see Propositions as Types for newer supplementary material.
The theorems we have seen so far have appeared rather ordinary, but their semantics suggests another kind of statement which is not. The interpretation we discuss below may seem problematic to the reader who is seeing constructive mathematics for the first time, so it may be useful for the new user to contrast the ideas below with the traditional, truth--functional view of the semantics of logic. In constructive logic a proposition is identified with the evidence we can give for it. Specifically, a proposition is a type consisting of formal objects called proofs . For example, the proofs corresponding to 0=0 in int and to int in U1 consist solely of the object axiom . It is important to note that although we think of statements of membership (e.g., 1 in int) or of equality (e.g., 0=0 in int) as being propositions, they are in fact types and they are combined with other types using type constructors. Later on we show how to define logical connectives in terms of type constructors so that we can combine these kinds of statements in the familiar fashion of sentential logic. As far as the Nuprl system is concerned, however, propositions are just types.
With this view of propositions, we lose some of the equivalences of classical logic. Thus, for example, if p is a proposition and represents its negation then p and are no longer equivalent. As types they are different, although from a classical, truth--functional point of view they are the same.
Not only can we assert types which correspond to propositions by exhibiting (either explicitly or implicitly) members of the type, but it makes sense to assert any type. To do so means that the type is inhabited. To prove the assertion is to produce an object, either implicitly or explicitly.