English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We investigate the elimination of quantifiers in first-order formulas viaHilbert's epsilon-operator (or -binder), following Bernays' explicitdefinitions of the existential and the universal quantifier symbol by means ofepsilon-terms. This elimination has its first explicit occurrence in the proofof the first epsilon-theorem in Hilbert-Bernays in 1939. We think that there isa lacuna in this proof w.r.t. this elimination, related to the erroneousassumption that explicit definitions always terminate. Surprisingly, to thebest of our knowledge, nobody ever proved confluence or termination for thiselimination procedure. Even myths on non-confluence and the openness of thetermination problem are circulating. We show confluence and termination of thiselimination procedure by means of a direct, straightforward, and easilyverifiable proof, based on a new theorem on how to obtain termination from weaknormalization.

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