Constructive Content of Classical Reasoning

Maria Napierala

The evidence for disjunction and existentially quantified proposition, as formalized in Prawitz natural deduction system for the first-order classical logic, is never used directly except to prove other propositions [1], [2]. Such interpretation gives the constructive meaning of these two most typically intuitionistic connectives without restricting the logic to be intuitionistic. It is a consequence of the non-uniform nature of the introduction rules for “there exists” and “or” in natural deduction, namely the introduction rule for “there-exists x. P(x)” has one assumption for every “a” with the property P and disjunction has two separate introduction rules for each disjunct. This fact, when combined with classical law of double negation elimination, implies that classical proofs, viewed as computations, can be multi-valued, e.g., encoding several witnesses for the same existential sentence. The elimination rules for “there-exists” and ∨ bring those disjoined assumptions together by means of a third formula which plays the role of a context of a proof of ”there-exists x. P(x)” or P ∨ Q. We observe that bringing those disjoined assumptions together can fundamentally be postponed. The moment of reunification can be chosen to be such that a proof (whether by double negation elimination or not) is well-typed. In contrast with disjunction, the proofs of conjunction P ∧ Q are always well-typed if the proofs of both, P and Q, are well-typed. In order for the proof of implication P ⟹ Q to be well-typed, the proofs of P have to be welltyped (whether P is proved by double negation elimination or not) which is accomplished by “unifying” them through Q. Hence, the classical implication provides the means of making the proofs of an arbitrary classical formula well-typed by constructing well-typed proof contexts. In particular, classical negation “not P” (interpreted as P ⟹ 0 where “0” stands for the absurdity) provides a well-typed top-level proof context for any PI(0,2) formula P. Finally, the constructive content of the classical rule of double negation elimination “not(notP) ⟹ P” is that it gives a proof of P access to its current proof context. Such a proof is well-typed if the formula P is in PI(0,2) class [3]. This constructive interpretation of negation and of the rule of double negation elimination depends on the logical constant the negation or double negation is applied to.

[1] Prawitz D. Natural deduction, a proof theoretic study. Almqvist and Winskell, 1965.

[2] Girard J-Y., Taylor P., Lafont,Y. Proofs and Types. Cambridge University Press. 1989.

[3] Kreisel G. Mathematical significance of consistency proofs. Journal of Symbolic Logic, 1958.

Address: AT& T Laboratories, 200 Laurel Avenue, Middletown, NJ 07748, USA

E-mail: mnapierala@att.com