The role of quantifier alternations in cut elimination

DOI10.1305/ndjfl/1117755147zbMath1078.03045MaRDI 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 elimination; proof complexity; quantifier alternations

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03F20: Complexity of proofs

Related Items

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

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