Extended normal form theorems for logical proofs from axioms
type: Item
instance of: scholarly article
title: Extended normal form theorems for logical proofs from axioms
zbMATH Open document ID: 0971.03059
DOI: 10.1016/S0304-3975(99)00172-3
author: Toshiyasu Arai
author: G. E. Mints
published in: Theoretical Computer Science
publication date: 2000-08-23T00:00:00Z
review text: The authors (and others) have been working on refinements of cut elimination and their implications. The main theorem of this paper states: if a sequent \(A_0,\dots, A_n\to A_{n+1}\) is provable (in predicate calculus), then it has an irreducible proof with respect to \(A_0,\dots,A_n\). Here, the \(A\)'s are sets of closed formulas, and a proof is said to be irreducible if it is cut-free, free variables in it are eigen-variables or occur in the endsequent, and the main formula of an inference has a descendent in \(A_{i+1}\), \(i\leq n\), and it is not provable or refutable from \(A_0,\dots,A_i\), according as the formula is in the antecedent or in the succedent. A consequence of this theorem is the \(\omega\)-consistency of PA. Another consequence of a proof -- which is in the fashion of Gentzen's second consistency proof -- is the provable equivalence (over PRA) of the theorem itself with the 2-consistency \(\text{RFN}_{\Sigma_2} (C_{n+1})\), for recursive \(A_0,\dots,A_n\). Here, `RFN' stands for `reflection scheme', and \(C_n\) is obtained successively from \(\text{PA}\) \((=C_1)\) by \(C_{n+1}: =\text{qf-Ind}+ C_n+\text{RFN}(C_n)\).
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F30
zbMATH DE Number: 1495207
zbMATH Keywords: normal form theorem
zbMATH Keywords: reflection scheme
zbMATH Keywords: \(\omega\)-consistency
MaRDI profile type: Publication
Wikidata QID: Q114655902
cites work: A normal form for arithmetical derivations implying the \(\omega\)-consistency of arithmetic
cites work: Q5528627
cites work: Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
cites work: A normal form for logical derivations implying one for arithmetic derivations
cites work: Proof theory. 2nd ed
full work available at URL: s0304-3975(99)00172-3
OpenAlex ID: W2028575408
description: scientific article; zbMATH DE number 1495207