Abstract: Hilbert's epsilon-calculus is based on an extension of the language of predicate logic by a term-forming operator . Two fundamental results about the epsilon-calculus, the first and second epsilon theorem, play a role similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure.
Recommendations
Cites work
- A termination proof for epsilon substitution using partial derivations
- Ackermann's substitution method (remixed)
- Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
- Hilbert's \(\varepsilon{}\)-operator and classical logic
- Hilbert's ϵ‐operator in intuitionistic type theories
- Hilbert's ‘Verunglückter Beweis’, the first epsilon theorem, and consistency proofs
- scientific article; zbMATH DE number 1215493 (Why is no real title available?)
- scientific article; zbMATH DE number 612169 (Why is no real title available?)
- scientific article; zbMATH DE number 627412 (Why is no real title available?)
- scientific article; zbMATH DE number 1497485 (Why is no real title available?)
- scientific article; zbMATH DE number 1418438 (Why is no real title available?)
- scientific article; zbMATH DE number 3300566 (Why is no real title available?)
- scientific article; zbMATH DE number 3195384 (Why is no real title available?)
- scientific article; zbMATH DE number 3032487 (Why is no real title available?)
- Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX
- Intuitionistic ϵ‐ and τ‐calculi
- Lower bounds for increasing complexity of derivations after cut elimination
- Lower Bounds on Herbrand's Theorem
- On the interpretation of non-finitist proofs–Part II
- The Logic of Choice
- Update procedures and the 1-consistency of arithmetic
Cited in
(35)- Completeness of indexed \(\varepsilon\)-calculus
- On the compressibility of finite languages and formal proofs
- A sequent-calculus based formulation of the extended first epsilon theorem
- A mathematical basis for egress complexity
- Herbrand's theorem as higher order recursion
- Ackermann's substitution method (remixed)
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- scientific article; zbMATH DE number 3849202 (Why is no real title available?)
- The epsilon-reconstruction of theories and scientific structuralism
- Epsilon Calculi
- A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
- Non-elementary speed-ups in logic calculi
- Complexity of Ehrenfeucht models
- The Rank Function and Hilbert'S Second ε-Theorem
- scientific article; zbMATH DE number 1341475 (Why is no real title available?)
- scientific article; zbMATH DE number 1140575 (Why is no real title available?)
- Unsound inferences make proofs shorter
- A note on a proof of Hilbert's second ε-theorem
- scientific article; zbMATH DE number 4120146 (Why is no real title available?)
- EPSILON THEOREMS IN INTERMEDIATE LOGICS
- An abstract form of the first epsilon theorem
- Semantics and proof theory of the epsilon calculus
- Expansion trees with cut
- Computer Science Logic
- Epsilon nets and union complexity
- scientific article; zbMATH DE number 3300566 (Why is no real title available?)
- VON NEUMANN’S CONSISTENCY PROOF
- Cut Elimination in ε‐Calculi
- Herbrand complexity and the epsilon calculus with equality
- Non-elementary compression of first-order proofs in deep inference using epsilon-terms
- On translations of epsilon proofs to LK
- A simplified proof of the epsilon theorems
- Epsilon calculus provides shorter cut-free proofs
This page was built for publication: The epsilon calculus and Herbrand complexity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q817706)
