DOWNLOAD

The theory of natural deduction of pure intuitionistic logic for the (-->, &, A)-fragment is very elegant. It includes a strong normalization theorem and a Church-Rosser property. This elegant treatment extends to pure second-order intuitionistic logic (Girard's polymorphic system F). The technical details are more complicated in this case because of the impredicativity of the second-order quantifier, but strong normalization (and Church-Rosser) still holds.

The other connectives (absurdity, disjunction, existential quantification), whose features are more typical of intuitionism, do not have such an elegant treatment. Girard sees their elimination rules as defective. In second-order logic, these conectives can be circumvented because they are definable in terms of the others. It is not widely known that these conectives can also be circumvented in the treatment of first-order logic if we embed it in a version of predicative second-order logic.

Our tutorial will explain these issues.

Bibliography:

F. Ferreira. "Comments on predicative logic," Journal of Philosophical Logic 35, pp. 1-8 (2006).

J.-Y. Girard et al. Proofs and Types, Cambridge University Press, 1989. D. Prawitz. Natural Deduction, Dover Publications, 2006.

W. Tait. "Intensional interpretation of functionals of finite type I," The Journal of Symbolic Logic 32, pp. 198-212 (1967)

A. S. Troelstra & H. Schwichtenberg. Basic Proof Theory, Cambridge University Press, 2000.