Hilbert's epsilon as an operator of indefinite committed choice

DOI10.1016/J.JAL.2007.07.009MaRDI QIDQ946570zbMATH OpenOpenAlexFDO

Authors Claus-Peter Wirth

Publication date 23 September 2008

Published in Journal of Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

automated theorem provingformal philosophy of languageHilbert's epsilon operatorhuman-oriented interactive theorem provingsemantics of natural languagetheories of truth and validity

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic of natural languages (03B65) Structure of proofs (03F07)

Abstract: Paul Bernays and David Hilbert carefully avoided overspecification of Hilbert's epsilon-operator and axiomatized only what was relevant for their proof-theoretic investigations. Semantically, this left the epsilon-operator underspecified. In the meanwhile, there have been several suggestions for semantics of the epsilon as a choice operator. After reviewing the literature on semantics of Hilbert's epsilon operator, we propose a new semantics with the following features: We avoid overspecification (such as right-uniqueness), but admit indefinite choice, committed choice, and classical logics. Moreover, our semantics for the epsilon supports proof search optimally and is natural in the sense that it does not only mirror some cases of referential interpretation of indefinite articles in natural language, but may also contribute to philosophy of language. Finally, we ask the question whether our epsilon within our free-variable framework can serve as a paradigm useful in the specification and computation of semantics of discourses in natural language.

Recommendations

• Hilbert's \(\varepsilon{}\)-operator and classical logic
• Hilbert's and in proof theory: a proof-theoretical representation of universal and existential statements
• Hilbert's ϵ‐operator in intuitionistic type theories
• Semantics and proof theory of the epsilon calculus
• Computer Science Logic

Cites work

• Automated deduction in classical and non-classical logics. Selected papers
• Automated deduction. A basis for applications. Vol. III: Applications
• Descente Infinie + Deduction
• Eine Termlogik mit Auswahloperator
• Grundlagen der Mathematik I
• Hilbert's \(\varepsilon{}\)-operator and classical logic
• scientific article; zbMATH DE number 3904557 (Why is no real title available?)
• scientific article; zbMATH DE number 3926869 (Why is no real title available?)
• scientific article; zbMATH DE number 3664336 (Why is no real title available?)
• scientific article; zbMATH DE number 42287 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 1341475 (Why is no real title available?)
• scientific article; zbMATH DE number 1066668 (Why is no real title available?)
• scientific article; zbMATH DE number 1950269 (Why is no real title available?)
• scientific article; zbMATH DE number 1548692 (Why is no real title available?)
• scientific article; zbMATH DE number 1552534 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 873140 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3300566 (Why is no real title available?)
• scientific article; zbMATH DE number 3309179 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3349763 (Why is no real title available?)
• scientific article; zbMATH DE number 3088180 (Why is no real title available?)
• Intuitionistic ϵ‐ and τ‐calculi
• Mengentheoretische Begründung der Logik
• The Logic of Choice
• Theorie der Logischen Auswahlfunktionen
• Unification under a mixed prefix

Cited in

(5)

• Hilbert's \(\varepsilon{}\)-operator and classical logic
• Herbrand's fundamental theorem in the eyes of Jean van Heijenoort
• On Bourbaki's axiomatic system for set theory
• Typed Hilbert epsilon operators and the semantics of determiner phrases
• \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps

This page was built for publication: Hilbert's epsilon as an operator of indefinite committed choice

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