The epsilon calculus and Herbrand complexity

DOI10.1007/s11225-006-6610-7zbMath1097.03049arXivmath/0510640OpenAlexW2031927644MaRDI QIDQ817706

Georg Moser, Richard Zach

Publication date: 17 March 2006

Published in: Studia Logica (Search for Journal in Brave)

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

zbMATH Keywords

proof complexityHerbrand's theoremepsilon theoremsHilbert's \(\varepsilon\)-calculus

Mathematics Subject Classification ID

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

Related Items (15)

On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem ⋮ Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ The epsilon-reconstruction of theories and scientific structuralism ⋮ EPSILON THEOREMS IN INTERMEDIATE LOGICS ⋮ Herbrand complexity and the epsilon calculus with equality ⋮ On the compressibility of finite languages and formal proofs ⋮ A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract) ⋮ UNSOUND INFERENCES MAKE PROOFS SHORTER ⋮ Non-elementary speed-ups in logic calculi ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs ⋮ Herbrand's theorem as higher order recursion ⋮ VON NEUMANN’S CONSISTENCY PROOF ⋮ Ackermann's substitution method (remixed) ⋮ Semantics and Proof Theory of the Epsilon Calculus ⋮ Expansion trees with cut

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Lower bounds for increasing complexity of derivations after cut elimination
• Hilbert's \(\varepsilon{}\)-operator and classical logic
• Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
• A termination proof for epsilon substitution using partial derivations
• Ackermann's substitution method (remixed)
• Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX
• Hilbert's ‘Verunglückter Beweis’, the first epsilon theorem, and consistency proofs
• Lower Bounds on Herbrand's Theorem
• Hilbert's ϵ‐operator in intuitionistic type theories
• The Logic of Choice
• Intuitionistic ϵ‐ and τ‐calculi
• On the interpretation of non-finitist proofs–Part II

This page was built for publication: The epsilon calculus and Herbrand complexity