The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating.

We investigate the elimination of quantifiers in first-order formulas via Hilbert’s epsilon-operator (or -binder), following Bernays’ explicit definitions of the existential and the universal quantifier symbol by means of epsilon-terms. This elimination has its first explicit occurrence in the proof of the first epsilon-theorem in Hilbert–Bernays in 1939. We think that there is a lacuna in this proof w.r.t. this elimination, related to the erroneous assumption that explicit definitions always terminate. Surprisingly, to the best of our knowledge, nobody ever published a confluence or termination proof for this elimination procedure; and even myths on non-confluence and the openness of the termination problem are circulating. We show confluence and termination of this elimination procedure by means of a direct, straightforward, and easily verifiable proof, based on a theorem on how to obtain termination from weak normalization.

Authors

• Claus-Peter Wirth

Keywords

• Hilbert–Bernays Proof Theory
• History of Proof Theory
• Hilbert’s epsilon
• Quantifier Elimination
• (Weak) Normalization
• Termination
• (Local) Confluence