Classical Natural Deduction

Jan von Plato

Prawitz (1965) added to intuitionistic natural deduction a rule of indirect proof restricted to atomic formulas. The resulting system admits the normalization of derivations for the ∨, ∃-free fragment of the language of predicate logic. In von Plato (1998) and Negri and von Plato (2001), Prawitz’ rule is generalized into a rule of excluded middle permitting to conclude a formula C in propositional calculus if C is derived from an atom P and from its negation. The rule is admissible for arbitrary propositional formulas.

A generalization of the rule of excluded middle is given that applies to quantified formulas also. The result is a normalizing system of classical natural deduction for the full language of predicate logic. Normal derivations are well-founded, possibly infinitary trees. An example shows how to apply classical natural deduction in the proof theory of arithmetic.

References

Negri, S. and J. von Plato (2001) Structural Proof Theory, Cambridge University Press, in press.

von Plato, J. (1998) Proof theory of full classical propositional logic, submitted.

Prawitz, D. (1965) Natural Deduction: A Proof-Theoretical Study. Almqvist & Wicksell, Stockholm.

Address: Department of Philosophy, PL 24, Unioninkatu 40 B, 00014 University of Helsinki, Finland

E-mail: vonplato@helsinki.fi