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