A sequent-calculus based formulation of the extended first epsilon theorem

DOI10.1007/978-3-319-72056-2_4MaRDI QIDQ1709688zbMATH OpenOpenAlexFDO

Authors Matthias Baaz, Alexander Leitsch, Anela Lolic

Publication date 6 April 2018

Full work available at URL https://doi.org/10.1007/978-3-319-72056-2_4

zbMATH Keywords

epsilon calculusextended first epsilon theoremHerbrand disjunctions

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03)

Recommendations

• The epsilon calculus and Herbrand complexity
• Describing proofs by short tautologies
• Extracting Herbrand disjunctions by functional interpretation
• Sequent forms of Herbrand theorem and their applications
• Herbrand's theorem as higher order recursion

Cited in

(10)

• Herbrand's theorem as higher order recursion
• Extracting Herbrand disjunctions by functional interpretation
• Epsilon-logic is more expressive than first-order logic over finite structures
• scientific article; zbMATH DE number 1507197 (Why is no real title available?)
• EPSILON THEOREMS IN INTERMEDIATE LOGICS
• An abstract form of the first epsilon theorem
• Herbrand complexity and the epsilon calculus with equality
• Non-elementary compression of first-order proofs in deep inference using epsilon-terms
• A simplified proof of the epsilon theorems
• The epsilon calculus and Herbrand complexity

This page was built for publication: A sequent-calculus based formulation of the extended first epsilon theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1709688)