A normal form for logical derivations implying one for arithmetic derivations

DOI10.1016/0168-0072(93)90188-JMaRDI QIDQ2367413zbMATH OpenOpenAlexFDO

Authors G. E. Mints

Publication date 9 August 1993

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(93)90188-j

zbMATH Keywords

constant normal conditioncut eliminationmain formula restrictionnormal form theoremproper variable conditionsystems of arithmetic

Mathematics Subject Classification ID

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

Review text

The main result of this paper is a refined normal form theorem: a provable sequent has a cut-free derivation with the proper variable condition (i.e. a variable in the derivation is either an eigenvariable or occurs in the last sequent) and with the main formula restriction (i.e., no main formula of the antecedent is derivable). The author first proves the existence of such a derivation model-theoretically, and then the normalization theorem (that giving a procedure for converting a given derivation into a normal one) via an infinitary calculus. The results and methods are applied to systems of arithmetic. One result is that a derivation in arithmetic can be replaced by one that satisfies the proper variable and the constant normal condition (i.e., in each induction rule the induction term contains a variable). As a consequence, an existential statement is provable without induction, if it is provable at all. A normal form theorem of a more elaborate kind is proved; and the extendability of these results to the intuitionistic and the higher-order system is explained.

Recommendations

• A normal form for arithmetical derivations implying the \(\omega\)-consistency of arithmetic
• scientific article; zbMATH DE number 1169377
• Extended normal form theorems for logical proofs from axioms
• Normal derivations and sequent derivations
• Normal forms in combinatory logic
• Normal forms for derivations in Arai's \(\text{AI}_\xi^-\)
• General normal forms for any additive logic
• Normal deduction in the intuitionistic linear logic
• Normal derivability in modal logic
• scientific article; zbMATH DE number 1420808

Cites work

• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• scientific article; zbMATH DE number 3241254 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3360143 (Why is no real title available?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Proof theory. 2nd ed
• Reduction of finite and infinite derivations

Cited in

(13)

• A conservative extension of a formal arithmetic
• Normal forms for derivations in Arai's \(\text{AI}_\xi^-\)
• A normal form for arithmetical derivations implying the \(\omega\)-consistency of arithmetic
• Extended normal form theorems for logical proofs from axioms
• Reduction of finite and infinite derivations
• The computational content of arithmetical proofs
• scientific article; zbMATH DE number 3941504 (Why is no real title available?)
• scientific article; zbMATH DE number 4039891 (Why is no real title available?)
• General normal forms for any additive logic
• Normalization Proof for Derivations in PA after P. Cohen
• From arithmetic expressions to propositional formulae
• Logical Approaches to Computational Barriers
• Normalization proof for Peano arithmetic

This page was built for publication: A normal form for logical derivations implying one for arithmetic derivations

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