Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi (Q1208732)

The whole paper consists of two parts and is of interest both to logicians and theoretical computer scientists; its purpose is to give a coherent and gentle exposition of the material dealing with constructive logics, typed \(\lambda\)-calculi and linear logic. This first part covers the background material on natural deduction, sequent calculus, typed \(\lambda\)-calculus, and provides an introduction to Girard's linear logic; it contains also nonstandard material such as contraction-free systems for intuitionistic logic and Girard's translation of classical logic into intuitionistic logic. The reader, who is assumed to have some familiarity with logic and \(\lambda\)-calculus, will find here a nice and deep treatment of these matters. Numerous proof systems, corresponding to the different logics or points of view: intuitionistic/classical, natural deduction/sequent calculus, cut-free/cut-with, contraction-free/contraction-with, etc., are presented and analyzed, and complete encodings of (natural-deduction) proofs in enriched \(\lambda\)-calculi are systematically provided. One aim of the author is to uncover the intuitions behind all those formal systems and the reader will find many enlightening comments on the introduction of the various concepts and on the choices made at the level of formal rules. As an illustration of the richness of the paper let us just mention that the last section, which is devoted to the interpretation of classical logic into intuitionistic logic, presents three ``standard'' \(\neg\neg\)- translations, due to Gentzen, Gödel and Kolmogorov, as well as Girard's translation, based on polarities of formulas. The second part of the paper should contain more current topics, such as linear logic, proof nets, geometry of interaction, and unified systems of logic.