A normal form for arithmetical derivations implying the -consistency of arithmetic

DOI10.21099/TKBJM/1496163242MaRDI QIDQ1375747zbMATH OpenOpenAlexFDO

Authors Kazuma Ikeda

Publication date 14 September 1998

Published in Tsukuba Journal of Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.21099/tkbjm/1496163242

zbMATH Keywords

\(\omega\)-consistencynormal form theoremPeano arithmeticstrongly irreducible derivations

Mathematics Subject Classification ID

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

Review text

A derivation in Peano Arithmetic PA is strongly irreducible (s.i.) if it does not contain redundant free variables, redundant inductions (induction term is closed), redundant cuts (no cut formula is obtained by induction) or \(\forall\)-antecedent with side formula derivable in PA. If an s.i. derivation of a sentence \(\neg \forall xA(x)\) is given, the lowermost \(\forall\)-antecedent inference has side formula \(A(n)\) underivable in PA. Hence the proposition SI stating that every derivable formula has an s.i. derivation implies \(\omega\)-consistency of PA. The author proves this proposition using induction up to \(\varepsilon_1\) by the method of Gentzen's second consistency proof. The proposition SI extends the reviewer's normal form theorem from Ann. Pure Appl. Log. 62, 65-79 (1993; Zbl 0786.03040). T. Arai noticed that SI can be extended from PA to any theory and even to any finite sequence of increasing theories. This extension has an easy model-theoretic proof using ideas of the reviewer's paper [loc. cit.].

Recommendations

• A normal form for logical derivations implying one for arithmetic derivations
• Normal forms for derivations in Arai's \(\text{AI}_\xi^-\)
• Arithmetical proofs of strong normalization results for symmetric lambda calculi
• Typed Lambda Calculi and Applications
• A note on how to extend Gentzen's second consistency proof to a proof of normalization for first order arithmetic
• scientific article; zbMATH DE number 1169377
• [Russian Text Ignored]
• Extension of the formal system of the theory of expressions with arities and its strong normalization property
• Towards a formal proof system for \(\omega\)-rational expressions
• scientific article; zbMATH DE number 3941526

Cited in

(7)

• Towards a formal proof system for \(\omega\)-rational expressions
• Normal forms for derivations in Arai's \(\text{AI}_\xi^-\)
• Extended normal form theorems for logical proofs from axioms
• A normal form for logical derivations implying one for arithmetic derivations
• scientific article; zbMATH DE number 3559519 (Why is no real title available?)
• scientific article; zbMATH DE number 598799 (Why is no real title available?)
• A normal form for arithmetical representation of \({\mathcal N}{\mathcal P}\)-sets

This page was built for publication: A normal form for arithmetical derivations implying the \(\omega\)-consistency of arithmetic

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