From Hauptsatz to Hilfssatz

Jan von Plato ()
Additional contact information
Jan von Plato: University of Helsinki, Department of Philosophy

A chapter in Gentzen's Centenary, 2015, pp 89-130 from Springer

Abstract: Abstract Gentzen found his original consistency proof of arithmetic late in 1934. His work in pure logic was a preliminary to the result. Archival sources show that the consistency proof was based on an explicit semantic notion of correctness as reducibility of sequents and a proof that steps of derivation maintain reducibility. A crucial point in the latter was Gentzen’s Hilfssatz that stated, in analogy to his famous Hauptsatz, that composition of sequents maintains reducibility. The Hilfssatz was needed essentially for the case of the rule of complete induction. It was the point at which Gentzen’s proof superseded standard arithmetic methods in favour of an induction on well-founded trees, i.e., what came later to be called bar induction. After criticisms by Bernays and Gödel, the first proof evolved into one based on transfinite induction. Traces of the Hilfssatz that was founded on intuitionistic ideas disappeared, and Gentzen developed instead transfinite induction further into a general ordinal proof theory.

Keywords: Reduction Procedure; Intuitionistic Logic; Natural Deduction; Sequent Calculus; Elimination Rule (search for similar items in EconPapers)
Date: 2015
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-3-319-10103-3_5

Ordering information: This item can be ordered from
http://www.springer.com/9783319101033

DOI: 10.1007/978-3-319-10103-3_5

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().