Herbrand complexity and the epsilon calculus with equality

DOI10.1007/s00153-023-00877-3OpenAlexW4385380237MaRDI QIDQ6178471

Georg Moser, Kenji Miyamoto

Publication date: 18 January 2024

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-023-00877-3

zbMATH Keywords

proof complexityHilbert's epsilon calculusHerbrand complexityepsilon theorems

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exact bounds on epsilon processes
• The predicate calculus with \(\varepsilon\)-symbol
• The epsilon calculus and Herbrand complexity
• Proof theory. 2nd ed
• The number of proof lines and the size of proofs in first order logic
• Lower bounds for increasing complexity of derivations after cut elimination
• Handbook of proof theory
• A sequent-calculus based formulation of the extended first epsilon theorem
• Extracting Herbrand disjunctions by functional interpretation
• Ackermann's substitution method (remixed)
• Zur Widerspruchsfreiheit der Zahlentheorie
• Theorie der Logischen Auswahlfunktionen
• Some results on speed-up
• Lower Bounds on Herbrand's Theorem
• Lower bounds to the size of constant-depth propositional proofs
• The Logic of Choice
• UNSOUND INFERENCES MAKE PROOFS SHORTER
• Intuitionistic Predicate Calculus with ^|^epsilon;-Symbol
• Intuitionistic ϵ‐ and τ‐calculi
• EPSILON THEOREMS IN INTERMEDIATE LOGICS
• Intuitionistic Existential Instantiation and Epsilon Symbol
• Semantics and Proof Theory of the Epsilon Calculus
• Foundations of Software Science and Computation Structures
• The substitution method
• Some Results on the Length of Proofs
• Cut Elimination in ε‐Calculi

This page was built for publication: Herbrand complexity and the epsilon calculus with equality