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