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

TL;DR

This paper proves that the process of eliminating quantifiers via Hilbert's epsilon-operator is both confluent and terminating, addressing longstanding uncertainties in the proof of the epsilon-theorem.

Contribution

It provides the first rigorous proof of confluence and termination for quantifier elimination via epsilon-terms, filling a notable gap in the foundational literature.

Findings

Proves confluence of epsilon-based quantifier elimination

Establishes termination of the elimination process

Addresses misconceptions about non-termination and non-confluence

Abstract

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 proved confluence or termination for this elimination procedure. 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 new theorem on how to obtain termination from weak normalization.