A Simplified and Improved Free-variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice.

Free variables occur frequently in mathematics and computer science with ad hoc and altering semantics. We present here the most recent version of our freevariable framework for two-valued logics with properly improved functionality, but only two kinds of free variables left (instead of three): implicitly universally and implicitly existentially quantified ones, now simply called “free atoms” and “free variables”, respectively. The quantificational expressiveness and the problem-solving facilities of our framework exceed standard first-order logic and even higher-order modal logics, and directly support Fermat’s descente infinie. With the improved version of our framework, we can now model also Henkin quantification, neither using any binders (such as quantifiers or epsilons) nor raising (Skolemization). Based only on the traditional ε-formula of Hilbert–Bernays, we present our flexible and elegant semantics for Hilbert’s ε as a choice operator 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 ε supports reductive proof search optimally.

Authors

• Claus-Peter Wirth

Keywords

• Logical Foundations
• Theories of Truth and Validity
• Formalized Mathematics
• Human-Oriented Interactive Theorem Proving
• Automated Theorem Proving
• Choice
• Hilbert’s epsilon-Operator
• Henkin Quantification
• Fermat’s Descente Infinie