Introduction à la théorie de la démonstration : Élimination des coupures, normalisation et preuves de cohérence

Paris: Vrin (2022)
  Copy   BIBTEX

Abstract

Cet ouvrage offre une introduction accessible à la théorie de la démonstration : il donne les détails des preuves et comporte de nombreux exemples et exercices pour faciliter la compréhension des lecteurs. Il est également conçu pour servir d’aide à la lecture des articles fondateurs de Gerhard Gentzen. L’ouvrage introduit également aux trois principaux formalismes en usage : l’approche axiomatique des preuves, la déduction naturelle et le calcul des séquents. Il donne une démonstration claire et détaillée des résultats fondamentaux du domaine : traduction de l’arithmétique classique vers l’arithmétique intuitionniste, élimination des coupures, théorème de normalisation et conduit ensuite pas à pas le lecteur vers l’exposé de la célèbre preuve de cohérence de Gentzen pour l’arithmétique de Peano du premier ordre. Il comble ainsi une importante lacune éditoriale en présentant à la fois la théorie structurelle et la théorie ordinale de la démonstration.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs.Paolo Mancosu, Sergio Galvan & Richard Zach - 2021 - Oxford: Oxford University Press. Edited by Sergio Galvan & Richard Zach.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Gentzen's Proof of Normalization for Natural Deduction.Jan von Plato & G. Gentzen - 2008 - Bulletin of Symbolic Logic 14 (2):240 - 257.
Gentzen's proof of normalization for natural deduction.Jan von Plato - 2008 - Bulletin of Symbolic Logic 14 (2):240-257.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Canonical proof nets for classical logic.Richard McKinley - 2013 - Annals of Pure and Applied Logic 164 (6):702-732.
Stable Harmony.Nils Kurbis - 2008 - In Peliš Michal (ed.), Logica Yearbook 2007.
Gentzen's proof systems: byproducts in a work of genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.

Analytics

Added to PP
2023-02-09

Downloads
10 (#1,160,791)

6 months
9 (#298,039)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Richard Zach
University of Calgary

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references