UNSOUND INFERENCES MAKE PROOFS SHORTER

DOI10.1017/jsl.2018.51zbMath1439.03095arXiv1608.07703OpenAlexW3101828175WikidataQ113858288 ScholiaQ113858288MaRDI QIDQ4628675

Juan P. Aguilera, Matthias Baaz

Publication date: 15 March 2019

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1608.07703

zbMATH Keywords

cut eliminationsequent calculuseigenvariable conditionunsound inferences

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

The number of axioms, Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \), Andrews Skolemization may shorten resolution proofs non-elementarily, EPSILON THEOREMS IN INTERMEDIATE LOGICS, Towards a proof theory for quantifier macros, Effective Skolemization, Non-transitive correspondence analysis, Herbrand complexity and the epsilon calculus with equality, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Note on the Benefit of Proof Representations by Name, Determinate logic and the axiom of choice

Cites Work

• Unnamed Item
• Unnamed Item
• The epsilon calculus and Herbrand complexity
• Lower bounds for increasing complexity of derivations after cut elimination
• Cut normal forms and proof complexity
• On the complexity of proof deskolemization
• On the non-confluence of cut-elimination
• Lower Bounds on Herbrand's Theorem