Gentzen's centenary : the quest for consistency / edited by Reinhard Kahle, Michael Rathjen.

Format:

Book

Contributor:

Kahle, Reinhard., Editor.

Rathjen, Michael, Editor.

Language:

English

Subjects (All):

Logic, Symbolic and mathematical.

Mathematical Logic and Foundations.

Mathematical Logic and Formal Languages.

Local Subjects:

Mathematical Logic and Foundations.

Mathematical Logic and Formal Languages.

Physical Description:

1 online resource (563 p.)

Edition:

1st ed. 2015.

Place of Publication:

Cham : Springer International Publishing : Imprint: Springer, 2015.

Language Note:

English

Summary:

Gerhard Gentzen has been described as logic’s lost genius, whom Gödel called a better logician than himself. This work comprises articles by leading proof theorists, attesting to Gentzen’s enduring legacy to mathematical logic and beyond. The contributions range from philosophical reflections and re-evaluations of Gentzen’s original consistency proofs to the most recent developments in proof theory. Gentzen founded modern proof theory. His sequent calculus and natural deduction system beautifully explain the deep symmetries of logic. They underlie modern developments in computer science such as automated theorem proving and type theory. .

Contents:

Part I Reflections

Gentzen’s Consistency Proof in Context, Reinhard Kahle

Gentzen’s Anti-Formalist Views, Michael Detlefsen

The Use of Trustworthy Principles in a Revised Hilbert’s Program, Anton Setzer

Part II Gentzen’s Consistency Proofs

On Gentzen’s First Consistency Proof for Arithmetic, Wilfried Buchholz

From Hauptsatz to Hilfssatz, Jan von Plato

A Note on How to Extend Gentzen’s Second Consistency Proof to a Proof of Normalization for First Order Arithmetic, Dag Prawitz

A Direct Gentzen-Style Consistency Proof for Heyting Arithmetic, Annika Siders

Gentzen’s Original Consistency Proof and the Bar Theorem, W.W. Tait

Goodstein’s Theorem Revisited, Michael Rathjen

Part III Results

Cut Elimination In Situ, Sam Buss

Spector’s Proof of the Consistency of Analysis, Fernando Ferreira

Climbing Mount ε_0, Herman Ruge Jervell

Semi-Formal Calculi and Their Applications, Wolfram Pohlers

Part IV Developments

Proof Theory for Theories of Ordinals III: Π_N-Reflection, Toshiyasu Arai

A Proof-Theoretic Analysis of Theories for Stratified Inductive Definitions, Gerhard Jäger and Dieter Probst

Classifying Phase Transition Thresholds for Goodstein Sequences and Hydra Games, Frederik Meskens and Andreas Weiermann

Non-deterministic Epsilon Substitution Method for PA and ID_1, Grigori Mints

A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis, Paulo Oliva and Thomas Powell

Well-Ordering Principles and Bar Induction, Michael Rathjen and Pedro Francisco Valencia Vizcaíno. .

Notes:

Description based upon print version of record.

Includes bibliographical references.

ISBN:

3-319-10103-X