Also see Classical Propositional Logic for a constructive formal meta-treatment in Nuprl4 of classical propositional logic.

next up previous contents index
Next: Other Logical Operators Up: Defining Logics Previous: Constructive Logic

Classical Logic

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 gif. The ``vel''   operator represents the classical   connective ``or''. gif The classical  notion of implication is usually called material  implication  and is defined in terms of vel just as shown in figure gif. 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 gif 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

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995