It is possible to express classical logic in
the Nuprl
system by
introducing appropriate definitions. More specifically, one can introduce a
logical connective to correspond to the classical ``or'' by defining the new
connective via the classical equivalence between ``or'' and a suitable
combination of ``not'' and ``and''.
Consider the additional logical operators defined in figure 
.
The ``vel'' operator represents the
classical connective ``or''.
The classical notion of implication
is usually called material implication
and is defined in terms of vel just as shown in figure .
Likewise, the classical idea of existence
is far different from the constructive notion of existence in that
we can prove something exists classically by merely showing that it is
contradictory for it not to exist.
This is precisely the meaning captured by the given definition.
Figure: Definitions for Classical Logic
Figure shows some of the laws of classical logic in our notation.
From a formal point of view the situation is clear. We have defined logical operators that obey the laws of classical logic and are thus complete for the classical concept of logical truth in the first--order case. We have given an explanation of these laws in terms of type--theoretic concepts. While this is not the usual explanation in terms of Tarski's truth semantics, it is an adequate explanation for first--order logic.
Figure: Some Laws of Classical Logic