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

Thu Sep 14 08:45:18 EDT 1995