Semantics and proof theory of the epsilon calculus

DOI10.1007/978-3-662-54069-5_4MaRDI QIDQ5224489zbMATH OpenOpenAlexFDO

Authors Richard Zach

Publication date 24 July 2019

Published in Logic and Its Applications (Search for Journal in Brave)

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

zbMATH Keywords

choice functionintuitionistic logicproofproof theorysequent calculus

Mathematics Subject Classification ID

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

Abstract: The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the epsilon-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic interpretations. The problems facing the development of proof-theoretically well-behaved systems are outlined.

Recommendations

• Computer Science Logic
• Epsilon Calculi
• scientific article; zbMATH DE number 4123698
• The epsilon calculus and Herbrand complexity
• Cut Elimination in ε‐Calculi

Cites work

• Choice functions and the anaphoric semantics of definite NPs
• Completeness of indexed \(\varepsilon\)-calculus
• Cut Elimination in a Gentzen-Style ε-Calculus Without Identity
• Cut Elimination in ε‐Calculi
• Epsilon-logic is more expressive than first-order logic over finite structures
• Foundations of Software Science and Computation Structures
• Heyting predicate calculus with epsilon symbol
• Hilbert's \(\varepsilon{}\)-operator and classical logic
• scientific article; zbMATH DE number 1150714 (Why is no real title available?)
• scientific article; zbMATH DE number 3300566 (Why is no real title available?)
• scientific article; zbMATH DE number 3032487 (Why is no real title available?)
• Intuitionistic ϵ‐ and τ‐calculi
• Non-determinism in logic-based languages
• The epsilon calculus and Herbrand complexity
• The Logic of Choice
• The predicate calculus with -symbol
• Theorie der Logischen Auswahlfunktionen

Cited in

(21)

• Completeness of indexed \(\varepsilon\)-calculus
• Grounding, quantifiers, and paradoxes
• Cubic differentials and hyperbolic convex sets
• Explicit provability and constructive semantics
• scientific article; zbMATH DE number 4123698 (Why is no real title available?)
• scientific article; zbMATH DE number 1341475 (Why is no real title available?)
• scientific article; zbMATH DE number 1140575 (Why is no real title available?)
• Intuitionistic ϵ‐ and τ‐calculi
• EPSILON THEOREMS IN INTERMEDIATE LOGICS
• A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's -terms
• Computer Science Logic
• An axiomatization of ECTL
• [Russian Text Ignored]
• Herbrand complexity and the epsilon calculus with equality
• A reassessment of cantorian abstraction based on the -operator
• Interoperability of proof systems with SC-TPTP
• Non-elementary compression of first-order proofs in deep inference using epsilon-terms
• Epsilon calculus provides shorter cut-free proofs
• Reasoning about Hilbert's choice operator in SMT
• The epsilon calculus and Herbrand complexity
• Hilbert's epsilon as an operator of indefinite committed choice

This page was built for publication: Semantics and proof theory of the epsilon calculus

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