@book{SR--2011--01,
year={2011},
author={Claus-Peter Wirth},
title={A Simplified and Improved Free-Variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice},
series={{SEKI Report SR--2011--01 (ISSN 1437--4447)}},
note={{\url{http://arxiv.org/abs/1104.2444}}},
abstract={Free variables occur frequently in mathematics and computer science with {\it ad hoc}\/ and altering semantics. We present the most recent version of our free-variable 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 and even higher-order modal logics, and directly support Fermat's {\em descente infinie}. With the improved version of our framework, we can now model also \henkin\ quantification, neither using quantifiers (binders) nor raising (Skolemization). We propose a new semantics for Hilbert's $\varepsilon$ 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 $\varepsilon$ supports reductive proof search optimally.},
keywords={{Logical Foundations; Theories of Truth and Validity; Formalized Mathematics; Human-Oriented Interactive Theorem Proving; Automated Theorem Proving; Hilbert's epsilon-Operator; Henkin Quantification; Fermat's {\em Descente Infinie}}},
publisher={{SEKI Publications}},
address={{DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str.\,5, D--28359 Bremen, Germany}},
}