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.