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

Dag Prawitz ()
Additional contact information
Dag Prawitz: Stockholms universitet, Filosfiska institutionen

A chapter in Gentzen's Centenary, 2015, pp 131-176 from Springer

Abstract: Abstract The purpose of this note is to show that the normalization theorem can be proved for first order Peano arithmetic by adapting to natural deduction the method used in Gentzen’s second consistency proof. Gentzen explained the intuitive idea behind his proof by informally arguing for the possibility of a normalization theorem of natural deduction, but what he actually proved was a special case of the Hauptsatz for a sequent calculus formalization of arithmetic. To transfer Gentzen’s method to natural deduction, I shall assign his ordinals to notations for natural deductions that use an explicit operation of substitution. The idea is first worked out for predicate logic. The main problems reside there and consist in finding a normalization strategy that harmonizes with the ordinal assignment. The result for predicate logic is then extended to arithmetic without effort, and thereby full normalization of natural deductions in first order arithmetic is achieved.

Keywords: Gentzen; Natural Deduction; Normalization Theorem; Sequent Calculus; Maximum Formula (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_6

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

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

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 ().