Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
type: Item
instance of: scholarly article
title: Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
zbMATH Open document ID: 0772.03026
DOI: 10.1016/0304-3975(93)90011-H
author: Jean Gallier
published in: Theoretical Computer Science
publication date: 1993-05-16T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03-01
zbMATH DE Number: 166975
zbMATH Keywords: proof systems
zbMATH Keywords: sequent calculi
zbMATH Keywords: Gödel's translations
zbMATH Keywords: constructive logics
zbMATH Keywords: typed \(\lambda\)-calculi
zbMATH Keywords: linear logic
zbMATH Keywords: natural deduction
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: classical logic
reviewed by: Chantal Berline
MaRDI profile type: Publication
cites work: Computational interpretations of linear logic
cites work: The lambda calculus, its syntax and semantics
cites work: Q5565113
cites work: Q4039813
cites work: Contraction-free sequent calculi for intuitionistic logic
cites work: Q3743300
cites work: Q5610986
cites work: Q3994895
cites work: Q5625124
cites work: Linear logic
cites work: Q3773876
cites work: A new constructive logic: classic logic
cites work: Q3922646
cites work: Q3997528
cites work: Q5812175
cites work: Q3997016
cites work: Linearizing intuitionistic implication
cites work: On an interpretation of second order quantification in first order intuitionistic propositional logic
cites work: Q5559220
cites work: Q5632554
cites work: Combinators, \(\lambda\)-terms and proof theory
cites work: Intensional interpretations of functionals of finite type I
cites work: Q5605873
cites work: Q4093416
cites work: Proof theory
cites work: Constructivism in mathematics. An introduction. Volume II
cites work: Q4877107
cites work: Logic and structure
cites work: Q5813185
cites work: A new algorithm for derivability in the constructive propositional calculus
cites work: The correspondence between cut-elimination and normalization
full work available at URL: 0304-3975(93)90011-h
OpenAlex ID: W2134699386
description: scientific article; zbMATH DE number 166975