Normalization proof for Peano arithmetic

DOI10.1007/S00153-015-0450-YMaRDI QIDQ892146zbMATH OpenOpenAlexFDO

Authors Annika Siders

Publication date 18 November 2015

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00153-015-0450-y

zbMATH Keywords

natural deductionnormalizationPeano arithmetic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30)

Review text

The main purpose of the paper is to prove normalization of Peano arithmetic formulated in a standard natural deduction with an ordinal assignment originating in Howard's normalization proof for Gödel's T. The result is a generalization of an argument found in an earlier paper by \textit{A. Kanckos} [Math. Log. Q. 56, No. 6, 611--624 (2010; Zbl 1219.03072)] where a consistency proof for Heyting arithmetic was given.

Recommendations

• A note on how to extend Gentzen's second consistency proof to a proof of normalization for first order arithmetic
• Consistency of Heyting arithmetic in natural deduction
• scientific article; zbMATH DE number 48365
• A formalization of Sambins's normalization for GL
• A normal form for logical derivations implying one for arithmetic derivations

Cites work

• A note on how to extend Gentzen's second consistency proof to a proof of normalization for first order arithmetic
• Consistency of Heyting arithmetic in natural deduction
• Gentzen's consistency proof without heightlines
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3328152 (Why is no real title available?)

Cited in

(5)

• scientific article; zbMATH DE number 3559519 (Why is no real title available?)
• scientific article; zbMATH DE number 598799 (Why is no real title available?)
• Normalization Proof for Derivations in PA after P. Cohen
• A note on how to extend Gentzen's second consistency proof to a proof of normalization for first order arithmetic
• Categorical structure in coherent theory of arithmetic

This page was built for publication: Normalization proof for Peano arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q892146)