Organized by Université de Montpellier and LIRMM-CNRS with the support of the ANR project Polymnie, June 10-12 will see a really neat workshop on the use of epsilons and choice functions. The program is now online; if you can, you should go.
This workshop aims at promoting work on Hilbert’s Epsilon in a number of relevant fields ranging from Philosophy and Mathematics to Linguistics and Informatics. The Epsilon and Tau operators were introduced by David Hilbert, inspired by Russell’s Iota operator for definite descriptions, as binding operators that form terms from formulae. One of their main features is that substitution with Epsilon and Tau terms expresses quantification. This leads to a calculus which is a strict and conservative extension of First Order Predicate Logic. The calculus was developed for studying first order logic in view of the program of providing a rigorous foundation of mathematics via syntactic consistency proofs. The first relevant outcomes that certainly deserve a mention are the two “Epsilon Theorems” (similar to quantifiers elimination), the first correct proof of Herbrand’s theorem or the use of Epsilon operator in Bourbaki’s Éléments de Mathématique. In nineties, renewing Russell’s ideas on definite descriptions, there has been some work on the interpretation of determiners and noun phrases with Hilbert’s epsilon. Nowadays the interest in the Epsilon substitution method has spread in a variety of fields : Mathematics, Logic, Philosophy, History of Mathematics, Linguistics, Type Theory, Computer science, Category Theory and others.
Beside the famous Grundlagen der Mathematik of Hilbert and Bernays, a general presentation of the topic can be found in the webpages of the Stanford Encyclopedia of Philosophy and Internet Encyclopedia of Philosophy.