The role of quantifier alternations in cut elimination

DOI10.1305/ndjfl/1117755147zbMath1078.03045OpenAlexW2078269136MaRDI QIDQ2565988

Philipp Gerhardy

Publication date: 28 September 2005

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1117755147

zbMATH Keywords

cut eliminationproof complexityquantifier alternations

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items

The small‐is‐very‐small principle, Transductions in arithmetic, Interpretability degrees of finitely axiomatized sequential theories, The second incompleteness theorem and bounded interpretations, On the elimination of quantifier-free cuts, Sufficient conditions for cut elimination with complexity analysis, Peano Corto and Peano Basso: A Study of Local Induction in the Context of Weak Theories, A complexity analysis of functional interpretations, On the form of witness terms, Corrected upper bounds for free-cut elimination, The Interpretation Existence Lemma, The arithmetics of a theory

Cites Work

• The unprovability of small inconsistency. A study of local and global interpretability
• Cut elimination and automatic proof procedures
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Computer Science Logic