Semantics and proof theory of the epsilon calculus

DOI10.1007/978-3-662-54069-5_4zbMATH Open1432.03114arXiv1610.06289OpenAlexW2533162327MaRDI QIDQ5224489FDOQ5224489

Authors: Richard Zach 

Publication date: 24 July 2019

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

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.

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

Recommendations

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

zbMATH Keywords

proof theoryintuitionistic logicsequent calculuschoice functionproof

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (14)

• [Russian Text Ignored]
• The epsilon calculus and Herbrand complexity
• Computer Science Logic
• Cubic differentials and hyperbolic convex sets
• Hilbert's epsilon as an operator of indefinite committed choice
• EPSILON THEOREMS IN INTERMEDIATE LOGICS
• Herbrand complexity and the epsilon calculus with equality
• An axiomatization of ECTL
• Grounding, quantifiers, and paradoxes
• Explicit provability and constructive semantics
• Title not available (Why is that?)
• Intuitionistic ϵ‐ and τ‐calculi
• Completeness of indexed \(\varepsilon\)-calculus
• A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's \(\varepsilon\)-terms

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)