The Explicit Definition of Quantifiers via Hilbert ’s ε is Confluent and Terminating

Claus-Peter Wirth

Dept. of Math., ETH Zurich, Rämistr. 101, 8092 Zürich,

Switzerland

                wirth@logic.at

SEKI Report SR–2015–02

SEKI Report http://wirth.bplaced.net/seki.html ISSN 1437-4447

SEKI is published by the following institutions:

German Research Center for Artificial Intelligence (DFKI GmbH), Germany

• Robert Hooke Str. 5, D–28359 Bremen
• Trippstadter Str. 122, D–67663 Kaiserslautern
• Campus D 3 2, D–66123 Saarbrücken

Jacobs University Bremen, School of Engineering & Science, Campus Ring 1, D–28759 Bremen, Germany

Universität des Saarlandes, FR 6.2 Informatik, Campus, D–66123 Saarbrücken, Germany

SEKI Editor:

Claus-Peter Wirth

E-mail: wirth@logic.at
WWW: http://wirth.bplaced.net

Please send surface mail exclusively to:

DFKI Bremen GmbH Safe and Secure Cognitive Systems Cartesium Enrique Schmidt Str. 5 D–28359 Bremen Germany

This SEKI Report successfully passed the following external anonymous referee process:

IfCoLog Journal of Logics and their Applications 3(4), 2016

The Explicit Definition of Quantifiers via Hilbert ’s ε is Confluent and Terminating

Claus-Peter Wirth

Dept. of Math., ETH Zurich, Rämistr. 101, 8092 Zürich, Switzerland

                    wirth@logic.at

Received Nov 17, 2015. Accepted after Revision, Feb. 15, 2016

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 published a confluence or termination proof 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 theorem on how to obtain termination from weak normalization.

Keywords: Hilbert–Bernays Proof Theory, History of Proof Theory, Hilbert’s epsilon, Quantifier Elimination, (Weak) Normalization, (Strong) Termination, (Local) Confluence.

1 Introduction

1.1 The Explicit Historical Source of the Problem

With “Hilbert–Bernays” we will designate the “bible of proof theory”, i.e. the twovolume monograph Grundlagen der Mathematik (Foundations of Mathematics) in its two editions [Hilbert & Bernays, 1934; 1939] and [Hilbert & Bernays, 1968; 1970].

On p.19f. of [Hilbert & Bernays, 1939], as well as on p. 20 of the second edition [Hilbert & Bernays, 1970], we read:

“Unser zweiter vorbereitender Schritt besteht in der Ausschaltung der Allund Seinszeichen. Wie im vorigen Abschnitt gezeigt wurde, können wir die Anwendung der Grundformeln (a), (b) und der Schemata (α), (β) des Prädikatenkalkuls mit Hilfe der ε-Formel und der expliziten Definitionen (ε_{1}), (ε_{2}) entbehrlich machen^{1}. Führen wir diese Ausschaltung der Grundformeln und Schemata für die Quantoren an der zu betrachtenden Ableitung der Formel � aus und ersetzen wir hernach jeden Ausdruck (�) �(�) durch �(ε_{�} \overline{�(�)} ), jeden Ausdruck (E �) �(�) durch �(ε_{�}�(�)), so gehen die aus (ε_{1}), (ε_{2}) durch Einsetzung gewonnenen Formeln in solche über, die durch Einsetzung aus der Formel A∼A entstehen. Die Quantoren werden durch dieses Verfahren gänzlich ausgeschaltet, so daß nunmehr gebundene Variablen ausschließlich in Verbindung mit dem ε-Symbol auftreten, und der Beweiszusammenhang nur durch Wiederholungen, Einsetzungen, Umbenennung gebundener Variablen und Schlußschemata stattfindet.”

“Our second preparatory step consists in the elimination of the universal and existential quantifier symbols. As shown in the previous section, we can dispense with the application of Formulas (a), (b) and Schemata (α), (β) of the predicate calculus if we use the ε-formula and the explicit definitions (ε_{1}), (ε_{2}). If we apply this elimination of basic formulas und schemata for the quantifiers to the formula � under consideration, and afterwards replace every expression (�) �(�) with �(ε_{�} \overline{�(�)} ), every expression (E �) �(�) with �(ε_{�}�(�)), then the formulas obtained from (ε_{1}), (ε_{2}) by substitution are turned into formulas obtained by substitution from the formula A∼A. By this procedure, the quantifiers are completely eliminated, so that bound variables may occur only in combination with the ε-symbol, and the interconnections of the proof may consist only of repetitions, substitutions, renaming of bound variables, and inference schemata.”

Note that the “A” is not a meta-variable here (such as “�” is a meta-variable for a formula, and “�” for a bound individual variable), but a concrete object-level formula variable. In a proof step called substitution either such a formula variable (which is always free) or a free individual variable is replaced everywhere in a formula with an arbitrary formula or term, respectively. Furthermore, note that “Schlußschema” (“inference schema”) is nothing but a short name for the inference schema of modus ponens.

Moreover, note that Note 1 actually occurs only in the second edition and reads “^{1}Vgl. S.15.” (“^{1}Cf. p.15.”). Neither on Page 15 — nor anywhere else in the volumes — can we find any further information, however, regarding the following immediate questions:

• In which order are the final replacements of the two explicitly mentioned forms of expressions to be applied in the elimination of quantifiers?

• Or are such eliminations independent of the order of the replacements in the sense that they always yield unique normal forms?

What we can actually find on Page 15 are the mentioned “explicit definitions (ε_{1}), (ε_{2})”, which describe the rewrite relation of these replacements. In the more modern notation we prefer for this paper, these explicit definitions read:

∃x. A ⇔ A{x ↦ εx. A} (ε_{1})

∀x. A ⇔ A{x ↦ εx. ¬A} (ε_{2})

Note that x is a meta-variable for individual variables (in the original: a concrete objectlevel, bound individual variable), and A is a meta-variable for formulas (in the original: a concrete object-level, singulary formula variable). The original version of (ε_{1}) literally reads: (Ex) A(x) ∼ A(ε_{x} A(x)).

Note that the formulas considered here and in what follows are always first-order formulas, extended with ε-terms and possibly also with free (second-order) formula variables. For our considerations in this paper, it does not matter whether we include such formula variables into our first-order formulas or not.

1.2 Subject Matter

What we will study in this paper is the question how the elimination of first-order quantifiers via their explicit definitions can take place.

Here we should recall that, in explicit definitions (contrary to recursive definitions), the symbol to be defined (here: ∃ or ∀), occurring on the left-hand side of an equation (the definiendum) must not re-occur in the term on the right-hand side (definiens).

In this standard terminology, (ε_{1}) and (ε_{2}) classify as explicit definitions, because ∃ and ∀ do not occur on the right-hand sides — at least not explicitly.

It is commonplace knowledge that (contrary to recursive or implicit definitions) explicit definitions are analytic (i.e. not synthetic) in the sense that they cannot contribute anything essential to our knowledge base — simply because any notion introduced by an explicit definition can be eliminated from any language (at least in principle) after replacing all definienda with their respective definientia.

For first-order terms the eliminability is indeed trivial, even for non-right-linear equations such as

russell(x) = mbp(x, x),

where the number of occurrences of defined symbols in x is doubled when rewriting with this equation; i.e., if n(t) denotes the number of explicitly defined symbols in the term t, then n(russell(t)) = n(t) + 1, whereas n(mbp(t, t)) ≥ 2 ∗ n(t).

The termination of a stepwise elimination by applying one equation after the other — until no defined symbols remain — does not crucially depend on whether we rewrite the defined symbols in t before we apply the equation for the defined term russell(t) or after. Indeed, the difference this alternative can make is only a duplication of the rewrite steps required for the normalization of t.

This argumentation, however, does not straightforwardly apply to our definitions (ε_{1}), (ε_{2}). Indeed, the instance of the first occurrence of the meta-variable A on the right-hand side is modified by a substitution that may introduce an arbitrarily large number of copies of the instance of A.

We will show in this paper, however, that rewriting of an arbitrary formula F with (ε_{1}), (ε_{2}) is always confluent and terminating. This means that, no matter in which order we eliminate the quantifiers, a resulting quantifier-free formula will always be obtained, and that this formula is a unique normal form for F.

1.3 A Lacuna in Hilbert–Bernays?

The fact that this rewriting is innermost terminating has been well known before, but none of the experts on Hilbert’s ε we consulted knew about the strong termination (i.e. termination independent of any rewriting strategy), and one of them even claimed that the rewriting would not be confluent.

As the proofs of the ε-theorems of [Hilbert & Bernays, 1939] show, Paul Bernays (1888–1977) was well aware of the influence of strategies on elimination procedures. The mathematical technology of the 1930s, however, makes it most unlikely that he could easily show the strong termination — let alone consider it to be trivial in the context of a textbook (such as Hilbert–Bernays).

Moreover, the actual formula language of Hilbert–Bernays strongly suggests an outermost strategy: A non-outermost rewriting typically requires the instantiation of A to formulas containing variables that are bound by the outer quantifiers and epsilons. Such an instantiation is not permitted in Hilbert–Bernays, however, because these additional variables must come from a set of variables different from the free individual variables, which are called bound individual variables and which are not permitted to occur free in a substitution for A. Thus, for an innermost rewriting in the predicate calculus of Hilbert–Bernays, we have to resort to multiple tacit applications of Rule (δ′) for a complete reconstruction of the whole outer part of the formula in each innermost rewrite step; for Rule (δ′) see e.g. Page 109 in [Hilbert & Bernays, 1968; 2016b].

All in all, the fact that neither the innermost rewriting strategy nor Rule (δ′) is mentioned in this context in [Hilbert & Bernays, 1939] makes it most likely that Bernays just relied here on his learning that explicit definitions always admit an elimination, which is actually not the case in general for higher-order definitions.

1.4 Alternative Proofs by Applying Theories of First- or Higher-Order Rewriting?

In this paper, we will approach our results directly, without applying the theory of firstor higher-order rewrite systems. Other options for obtaining the crucial termination result could be:

1. To map the first-order terms with quantifiers and epsilons to quantifier- and epsilonfree first-order terms, to find a first-order term rewriting system that admits the transitive reduction of the images of any original reduction, and to prove the termination of the first-order term rewriting system, using the powerful theorems and methods to establish termination of first-order term rewriting systems (or even some of the software systems that may show first-order termination automatically, cf. e.g. [Winkler &al., 2013]).

2. To apply some results on termination of higher-order rewriting systems.

3. To map the first-order terms with quantifiers and epsilons to Church’s simply-typed λ-calculus (which is known to be terminating), such that the images of each original reduction admit the transitive reduction in simply-typed λ-calculus.

Let us look at second-order formulations of (ε_{1}), partly because the original formulation of Hilbert’s ε as found in [Ackermann, 1925] and [Hilbert, 1926; 1928] is already a second-order one without binders, and partly to develop options 2 and 3 a bit further.

If we use i to designate the sort (basic type) of individuals and o to designate the sort of formulas (as standard in Church’s simply-typed λ-calculus), then the ε gets the typing of ε : (i → o) → i, and for a second-order variable A : i → o and the existential operator Σ : (i → o) → o, we get

ΣA = A(εA),

or in η-expanded form

Σλx.(Ax) = A(ελx.(Ax)).

To implement these equations according to option 2, we have to pick one of the three competing higher-order rewriting frameworks, namely combinatory reduction systems (CRSs) [Klop, 1980], [Klop &al., 1993], higher-order rewrite systems [Nipkow, 1991], [Raamsdonk, 1999], and algebraic-functional systems [Jouannaud & Okada, 1991]. We pick the CRS framework because it is the oldest and most popular one (also admitting extension to conditional rewriting straightforwardly, cf. [Wirth, 2009, Note 9]).

In CRS syntax (cf. e.g. [Klop &al., 1993, § 11]), the η-expanded rule reads

Σ[x](A(x)) = A(ε[x](A(x))),

where x is a variable, A is a singulary meta-variable (not only a top-level one, but also w.r.t. the special technical terms used for CRSs, i.e. a meta-variable for a special variable that must not occur in the terms in the range of the rewrite relation), Σ and ε are singulary function symbols (i.e. 1-ary constant symbols), and [x] is an abstraction operator, binding the variable x. In this notation, we indeed have a CRS rewrite rule with the intended rewrite relation. We can formulate (ε_{2}) in a similar way, resulting in a two-rule CRS that is orthogonal (called “regular” in [Klop, 1980]), i.e. non-overlapping (“non-ambiguous”) and left-linear. Thus, according to [Klop &al., 1993, Corollary 13.6] ([Klop, 1980, Theorem II.3.11]), the rewrite relation is confluent.

As it is obvious that this rewrite relation is weakly normalizing (as it is innermost terminating), its termination (strong normalization) follows from Theorem II.5.9.3 of [Klop, 1980, p.168], provided that we can show our rewrite relation to be non-erasing. This means that we have to show that the set of free variables is invariant under rewrite steps. Note that the instance of A may contain free variables (such as y), but even if the instance of A is, say, \underline{λ}[x](y = y) (i.e. the quantifier is vacuous, binding a variable that does not occur in its scope), it seems that the deletion of the second occurrence of A in the righthand side does not matter, because all occurrences of free variables are preserved by the first occurrence of A in the right-hand side.

This argumentation, however, forgets that CRSs come without β-reduction. So we may need the rule (λ[x](A(x)))B = A(B) in addition, which would render the CRS erasing. On the other hand, \underline{λ} is different from λ (although some crucial underlining of λ is missing in [Klop &al., 1993]) and part and parcel of the substitution framework for “meta-variables” in [Klop &al., 1993]; this means we should get along without the β-rule for λ, provided that we write existential quantification in our formulas as, say, “Σ[x]” instead of “Σλx.”.

If the latter is indeed the case, and if our understanding of [Klop, 1980] is the right one, then confluence and termination can be established by applying the theory of CRSs.

As the contacted experts on higher-order rewriting did not want to help settling these questions (and no answer was found in [Raamsdonk, 2001], [Ketema & Raamsdonk, 2004] either), and as the effort to familiarize oneself (again) with the most fascinating and outstanding work documented in the PhD thesis [Klop, 1980] is considerable and disproportionate for our subject matter, we will present here a straightforward and efficiently verifiable proof of termination and confluence of the reduction relation defined directly on first-order terms with quantifiers and epsilons.

To implement option 3, however, we could to take ε as a constant with the above typing and the mapping to Church’s simply-typed λ-calculus could replace the previous constant Σ with the λ-term λA. (A(εA)) of the same type as Σ before. Then reduction by the first of the above equations could be done by a first β-reduction, and a second β-reduction on the λ-term A could be used to reduce A(εA), such that an original reduction step with (ε_{1}) results in two β-reduction steps after the mapping to simply-typed λ-calculus. Although this proof plan is most promising, it is not easily accessible in the sense that a mathematician could verify it without a careful formalization of lots of technical and syntactic details. Moreover, as Bernays in the 1930s could not have known about the termination of simply-typed λ-calculus — first shown by Tait [1967] — this is not a proof plan he could have followed (though he was in correspondence with Church and visiting the Institute for Advanced Study in Princeton during session 1935/36).

Finally, note that — compared to options 1–3 — our direct and efficiently verifiable procedure is not only more informative on the concrete structure of the particular subject matter, but also the stronger, more concise, and historiographically more relevant evidence against myths on Hilbert–Bernays with regard to non-confluence and openness of the termination question.

2 Background and Tools

2.1 Basic Notions and Notation

We follow standard mathematical writing style, cf. [Gillman, 1987].

We try to be self-contained in this this paper. In case we should omit some required information, we refer the reader to the survey [Klop, 1980, § I.5] on abstract rewrite systems.

Let ‘N’ denote the set of natural numbers, and ‘<’ the ordering on N. Let N_{+} := { n ∈ N | 0 ≠ n }.

For classes R, A, and B we define:

dom(R) := { a | ∃b. (a, b) ∈ R }  domain
A↿R := { (a, b) ∈ R | a ∈ A } (domain-) restriction to A
⟨A⟩R := { b | ∃a ∈ A. (a, b) ∈ R }  image of A, i.e. ⟨A⟩R = ran(_{A}↿R)

And the dual ones:

ran(R) := { b | ∃a. (a, b) ∈ R }  range
R↾_{B} := { (a, b) ∈ R | b ∈ B } range-restriction to B
R⟨B⟩ := { a | ∃b ∈ B. (a, b) ∈ R } reverse-image of B, i.e. R⟨B⟩ = dom(R↾_{B})

We use ‘id’ for the identity function, and ‘∘’ for the composition of binary relations. Functions are (right-) unique relations, and so the meaning of “f∘g ” is extensionally given by (f∘g)(x) = g(f(x)).

Let ⟶ be a binary relation. ⟶ is a relation on A if dom(⟶) ∪ ran(⟶) ⊆ A. ⟶ is irreflexive if id∩⟶ = ∅. It is A-reflexive if _{A}↿id ⊆ ⟶. Speaking of a reflexive relation we refer to the largest A that is appropriate in the local context, and referring to this A we write ⟶^{0} to ambiguously denote _{A}↿id. With ⟶^{1} := ⟶, and ⟶^{n+1} := ⟶^{n}∘⟶ for n ∈ N_{+}, ⟶^{m} denotes the m-step relation for ⟶. The transitive closure of ⟶ is ⟶^{+} := ⋃_{n∈N_{+}} ⟶^{n}. The reflexive closure of ⟶ is ⟶^{=} := ⋃_{n∈{0,1}} ⟶^{n}. The reflexive transitive closure of ⟶ is ⟶^{∗} := ⋃_{n∈N} ⟶^{n}. The reverse of ⟶ is ⟵ := { (b, a) | (a, b) ∈ ⟶ }.

v and w are called joinable w.r.t. ⟶ if v↓w, i.e. if v⟶^{∗} ∘ ⟵^{∗}w. ⟶ is locally confluent if v↓w for any v, w with v⟵ ∘ ⟶w; it is confluent if v↓w for any v, w with v⟵^{∗} ∘ ⟶^{∗}w. a′ is an ⟶-normal form of a if a⟶^{∗}a′ ∉ dom(⟶).

A sequence (s_{i})_{i∈N} is non-terminating in ⟶ if s_{i}⟶s_{i+1} for all i ∈ N. ⟶ is terminating if there are no non-terminating sequences in ⟶. A relation R (on A) is well-founded if any non-empty class B (⊆A) has an R-minimal element, i.e. ∃a ∈ B. ¬∃a′ ∈ B. a′R a. Note that well-foundedness of ⟵ immediately entails termination of ⟶ (via the range of the non-terminating sequence), but the converse requires a weak form of the Axiom of Choice to construct the non-terminating sequence, cf. e.g. [Moore & Wirth, 2014, § 4.1].

Corollary 2.1 If a binary relation is well-founded, so is its transitive closure.

2.2 A Generalized Theorem as the Main Tool

The following Theorem 2.2 is a generalization of Jan Willem Klop’s Theorem I.5.18 [Klop, 1980, p. 53], which can be obtained again from Theorem 2.2 by the specializa-

tion ⟶_{0} := ∅.

Theorem 2.2 Let ⟶_{0} and ⟶_{1} be two binary relations.

Set ⟶_{2} := ⟶^{∗}_{0} ∘ ⟶_{1}.

Set ⟶_{3} := ⟶_{0} ∪ ⟶_{1}.

Let a ∈ dom(⟶_{3}). Let a′ be an ⟶_{3}-normal form of a. Set A := ⟨{a}⟩⟶^{∗}_{3}.

Set ⟶_{4} := _{A}↿⟶_{3}. If

1. ⟵_{0}↾_{A} is well-founded;

2. there is an upper bound n ∈ N on the length of ⟶_{2}-derivations starting from a and reaching a′ by ⟶^{∗}_{0}; more formally, this means that we have m ≤ n for any m ∈ N

and any sequence b_{0}, …, b_{m} with a = b_{0}, b_{i}⟶_{2}b_{i+1} for each i ∈ {0, …, m−1}, and

b_{m}⟶^{∗}_{0}a′;

3. for all b_{1}, b_{2} with b_{1}⟵_{4} ∘ ⟶_{1}b_{2}, we have b_{1}⟶^{∗}_{4} ∘ ⟵^{∗}_{4}b_{2}; and

4. for all b_{1}, b_{2} with b_{1}⟵_{4} ∘ ⟶_{0}b_{2}, we have b_{1}⟶^{∗}_{4} ∘ ⟵^{=}_{4}b_{2};

then ⟵_{4} is well-founded.

Proof of Theorem 2.2

\underline{\underline{Claim 1:}} For all b_{1}, b_{2} and n ∈ N with b_{1}⟵_{4} ∘ ⟶^{n}_{0}b_{2}, we have b_{1}⟶^{∗}_{4} ∘ ⟵^{=}_{4}b_{2}.

\underline{\underline{Proof of Claim 1:}} By induction on n. In case of b_{1}⟵_{4} ∘⟶^{0}_{0}b_{2}, we have b_{1}⟵_{4}b_{2}. In case

of b_{1}⟵_{4}∘⟶^{n}_{0}b_{2}⟶_{0}b_{3}, by induction hypothesis we have b_{1}⟶^{∗}_{4}b_{4}⟵^{=}_{4}b_{2}

for some b_{4} ∈ A. In case of b_{4} = b_{2}, we have b_{1}⟶^{∗}_{4}b_{4}⟶_{0}b_{3}, and thus b_{1}⟶^{∗}_{4}b_{3}. Otherwise, we have b_{4}⟵_{4}b_{2}, and thus b_{4}⟶^{∗}_{4}b_{5}⟵^{=}_{4}b_{3} for some b_{5} by item 4, i.e. the desired

b_{1}⟶^{∗}_{4}b_{5}⟵^{=}_{4}b_{3}. \underline{\underline{Q.e.d. (Claim 1)}}

Set B := { b ∈ A | b⟶^{∗}_{4}a′ }.

By item 2, we can define a function l : B → { m ∈ N | m ≤ n } via

l(b) := max { m ∈ N | b⟶^{m}_{2} ∘ ⟶^{∗}_{0}a′ }.

\underline{\underline{Claim 2:}} For all b ∈ B with b⟶^{∗}_{4}b′, we have b′ ∈ B.

\underline{\underline{Proof of Claim 2:}} By induction on k := l(b) in <. The induction hypothesis is that for

all b′′ ∈ B with b′′⟶^{∗}_{4}b′′′ and l(b′′) < k, we have b′′′ ∈ B. Note

that (for b′′ ∈ B) b′′⟶_{4}b′′′ implies l(b′′′) ≤ l(b′′). Thus, by another induction on the length of derivations, the induction conclusion follows from the induction hypothesis and the proposition that for all b′′ ∈ B with b′′⟶_{4}b′′′ and l(b′′) = k, we have b′′′ ∈ B. So let us assume b ∈ B and b⟶_{4}b′. Then, using the induction hypothesis, we have to show b′ ∈ B, for which it suffices to show b′⟶^{∗}_{4}a′. By our assumption, we have b⟶^{∗}_{4}a′, which falls into at least one of the following two cases:

\underline{b⟶^{∗}_{0}a′ :} By Claim 1: b′⟶^{∗}_{4} ∘ ⟵^{=}_{4}a′. Because a′ ∉ dom(⟶_{3}), and a fortiori also a′ ∉ dom(⟶_{4}), we actually have b′⟶^{∗}_{4}a′.

\underline{b⟶^{∗}_{0}b̂⟶_{1}b′′′⟶^{∗}_{4}a′ for some b̂, b′′′ :} Again by Claim 1, we get b′⟶^{∗}_{4}b′′′′⟵^{=}_{4}b̂ for some

b′′′′ ∈ A.

In case of b′′′′ = b̂, we have b′⟶^{∗}_{4}b′′′′⟶_{1}b′′′⟶^{∗}_{4}a′, i.e. the desired b′⟶^{∗}_{4}b′′′′⟶_{4}b′′′⟶^{∗}_{4}a′.

Otherwise we have b′′′′⟵_{4}b̂. Thus, by item 3, there is some b′′ with b′′′′⟶^{∗}_{4}b′′⟵^{∗}_{4}b′′′. Because of b⟶^{∗}_{0}b̂⟶_{1}b′′′⟶^{∗}_{4}a′ we have b′′′ ∈ B and l(b′′′) < l(b). Thus, by the induction hypothesis, we get b′′ ∈ B, and then the desired b′⟶^{∗}_{4}b′′′′⟶^{∗}_{4}b′′⟶^{∗}_{4}a′. \underline{\underline{Q.e.d. (Claim 2)}}

\underline{\underline{Claim 3:}} A = B.

\underline{\underline{Proof of Claim 3:}} By a⟶^{∗}_{3}a′, we also have a⟶^{∗}_{4}a′, and so a ∈ B.

Thus, by Claim 2, we get ⟨{a}⟩⟶^{∗}_{4} ⊆ B.

All in all, we get: A = ⟨\{a\}⟩⟶^{∗}_{3} = ⟨\{a\}⟩⟶^{∗}_{4} ⊆ B ⊆ A. \underline{\underline{Q.e.d. (Claim 3)}}

By Claim 4, we get l : A → { m ∈ N | m ≤ n }. Now for every b_{1}, b_{2} with b_{1}⟵_{4}b_{2}, we have b_{1}, b_{2} ∈ A and, moreover, (l(b_{1}), b_{1}) is strictly smaller than (l(b_{2}), b_{2}) in the lexicographic combination of < and ⟵_{0}↾_{A}, which is well-founded by item 1. Indeed, in case of b_{1}⟵_{0}b_{2}, we have l(b_{1}) ≤ l(b_{2}) and b_{1}⟵_{0}↾_{A}b_{2}, and in case of b_{1}⟵_{1}b_{2}, we have l(b_{1}) < l(b_{2}). Q.e.d. (Theorem 2.2)

2.3 Terms, Formulas, Substitutions, Contexts

A straightforward intuitive understanding of terms, formulas, substitutions, and contexts will actually suffice for most working mathematicians to understand the remainder of this paper. For the others, we give an example formalization of these notions here.

Terms and formulas are defined inductively as follows:

• An individual variable is a term.

• If A is an n-ary formula variable (n ∈ N) and t_{1}, …, t_{n} are terms, then A(t_{1}, …, t_{n}) is a formula.

• If f is an n-ary constant function or predicate symbol (n ∈ N) and t_{1}, …, t_{n} are terms, then f(t_{1}, …, t_{n}) is a term or formula, respectively. In case of n = 0, we simply write “f” instead of “f()”.

• If F is a formula, then ¬F is a formula. If F_{1} and F_{2} are formulas, then (F_{1}∨F_{2}), (F_{1}∧F_{2}), (F_{1}⇒F_{2}), … are formulas.

• If x is an individual variable and F is a formula, then εx. F is a term and ∃x. F and ∀x. F are formulas. In these terms and formulas, all occurrences of x are bound; non-bound occurrences of variables in terms and formulas are called free, such as each occurrence of any formula variable, and also of any individual variable y that is not in the scope of a binder on y, such as “εy.”, “∃y.”, or “∀y.”.

In our definition of terms and formulas we deviate from Hilbert–Bernays in not having an extra set of individual variables for bound occurrences, disjoint from the set to be used for free occurrences. So we have only one set of individual variables, but this does not really make any difference here, in particular because we ignore the variable names in the bound occurrences by the following stipulation:

We equate formulas modulo the renaming of bound variables.

A substitution is a mapping of individual variables to terms and of n-ary formula variables to expressions of the form \underline{λ}(x_{1}, ⋯, x_{n}). F, respectively, where x_{1}, ⋯, x_{n} are mutually distinct individual variables and F is a formula. For n = 0, we just write “F ” instead of “\underline{λ}(). F ”.

Presupposing the above stipulation of considering formulas only up to renaming of bound variables, we now define the result of an application of a substitution σ to terms and formulas inductively as follows. We use postfix notation with highest operator precedence.

• Let x be an individual variable.

If x ∉ dom(σ), then xσ = x; otherwise xσ = σ(x), i.e. the value of x under σ.

• Let A be an n-ary formula variable, and let t_{1}, …, t_{n} be terms. If A ∉ dom(σ), then (A(t_{1}, …, t_{n}))σ = A(t_{1}σ, …, t_{n}σ). Otherwise (A(t_{1}, …, t_{n}))σ is the result of the β-reduction of σ(A)(t_{1}σ, …, t_{n}σ), i.e., for σ(A) = \underline{λ}(x_{1}, ⋯, x_{n}). F, the formula F σ′, where σ′ is the substitution {x_{1} ↦ t_{1}σ, …, x_{n} ↦ t_{n}σ}.

• If f is an n-ary constant function or predicate symbol and t_{1}, …, t_{n} are terms, then (f(t_{1}, …, t_{n}))σ = f(t_{1}σ, …, t_{n}σ).

• If F is a formula, then (¬F)σ = ¬F σ. If F_{1} and F_{2} are formulas, then (F_{1}∨F_{2})σ = (F_{1}σ∨F_{2}σ), (F_{1}∧F_{2})σ = (F_{1}σ∧F_{2}σ), (F_{1}⇒F_{2})σ = (F_{1}σ⇒F_{2}σ), ….

• If x is an individual variable — w.l.o.g. neither an element of dom(σ), nor occurring (free) in ran(σ) — and F is a formula, then (εx. F)σ = εx. F σ, (∃x. F)σ = ∃x. F σ, (∀x. F)σ = ∀x. F σ.

Corollary 2.3 If X is an individual variable or a nullary formula variable, and σ is a substitution, then for any formula or term G whose free variables are in A: Gσ = G(_{A}↿σ).

By induction on the construction of G_{1} we easily get:

Corollary 2.4 For any term or variable G_{1}, any X and G_{2} being either an individual variable and a term, or a nullary formula variable and a formula, and any substitution σ where X ∉ dom(σ) and X does not occur (free) in ran(σ) : (G_{1}{X↦G_{2}})σ = (G_{1}σ){X↦G_{2}σ}.

Finally, let H_{0}, …, H_{n} (n ∈ N) be mutually distinct, nullary formula variables, reserved for the following definition: A context written “G[⋯]” (a formula or term with holes) is actually a formula or term G with one single (free) occurrence of each of the formula variables H_{1}, …, H_{n}. Moreover, “G[F_{1}, …, F_{n}]” denotes G{H_{1}↦F_{1}, …, H_{n}↦F_{n}}, for formulas F_{1}, …, F_{n}.

Corollary 2.5 For any context G[⋯], and any formula F, and any substitution σ : (G[F])σ = Gσ[F σ].

3 The Concrete Rewrite Relation

By writing “¬^{∀}” for “¬” and “¬^{∃}” for the empty string “ ”, we can unify the two formulas (ε_{1}) and (ε_{2}) to the single formula

Qx. A ⇔ A{x ↦ εx. ¬^{Q}A} (ε_{Q})

for Q ∈ {∃, ∀}, and x a meta-variable for an individual variable, and A a meta-variable for a formula.

Let ⟶ be the rewrite relation resulting from rewriting with the equivalence (ε_{Q}) as a rewrite rule from left to right. Explicitly, this means that F_{1}⟶F_{2} if there are a context G[⋯], a quantifier symbol Q, an individual variable x, and a formula A, such that F_{1} = G[Qx. A] and F_{2} = G[A{x ↦ εx. ¬^{Q}A}].

Let ⟶_{0} and ⟶_{1} be the partition of ⟶ for the case of a vacuous quantifier (i.e. for the case that x does not occur in the formula A in (ε_{Q})), and for the case that the quantifier is not vacuous.

Let ⟶_{I} be the innermost rewrite relation given by rewriting with the equivalence (ε_{Q}).

Let ⟶ ∥ be the version of ⟶ for the rewriting of parallel redexes. Explicitly, this means that F_{1}⟶ ∥ F_{2} if there are a context G[⋯] with n ∈ N holes, quantifier symbols Q_{1}, …, Q_{n}, individual variables x_{1}, …, x_{n}, and formulas A_{1}, …, A_{n}, such that

\begin{aligned}F_{1} & = & G[Q_{1}x_{1}. A_{1}, …, Q_{n}x_{n}. A_{n}], \\ F_{2} & = & G[A_{1}\{x_{1} ↦ εx_{1}. ¬^{Q_{1}}A_{1}\}, …, A_{n}\{x_{n} ↦ εx_{n}. ¬^{Q_{n}}A_{n}\}]. \end{aligned}

From these definitions, we immediately get the following corollaries.

Corollary 3.1 ⟶_{I} ⊆ ⟶.

Corollary 3.2 ⟶ ∥ ⊆ ⟶^{∗}.

3.1 Local Confluence

Note that the technical terms of the following lemma are clarified and formalized in its proof.

Lemma 3.3 If we have a peak F_{1}⟵F_{0}⟶F_{2} of local divergence and the redex of the rewrite step to F_{1} is properly inside the one of the rewrite step to F_{2} (which is on top of F_{0}), then there are formulas F_{3}, F_{4} satisfying all the following items:

1. F_{1}⟶F_{4}⟵F_{3}⟵ ∥ F_{2}.

2. If the initial step to the left is actually applied to a non-vacuous quantifier (i.e. if F_{1}⟵_{1}F_{0}), then we have F_{4}⟵_{1}F_{3}⟵ ∥ _{1}F_{2}.

3. If the initial step to the right is actually applied to a non-vacuous quantifier (i.e. if F_{0}⟶_{1}F_{2}), then we have F_{1}⟶_{1}F_{4}.

4. If the initial step to the right is actually applied to a vacuous quantifier (i.e. if F_{0}⟶_{0}F_{2}), then we have F_{3} = F_{2}.

Proof of Lemma 3.3

Suppose we have a peak F_{1}⟵F_{0}⟶F_{2} of local divergence and the redex of the rewrite step to F_{1} is properly inside the one of the rewrite step to F_{2}, which is on top of F_{0}. Then

F_{0} has the form Q_{1}x_{1}. G_{1}[Q_{2}x_{2}. G_{2}]. (F_{0})

We may in particular assume here that x_{2} is different from x_{1} and does not occur free in the context G_{1}[⋯] if we consider the dots “⋯” to be empty. Moreover we may assume that the formulas F_{1} and F_{2} are the following:

Q_{1}x_{1}. G_{1}[G_{2}{x_{2} ↦ εx_{2}. ¬^{Q_{2}}G_{2}}]. (F_{1})

( G_{1}[Q_{2}x_{2}. G_{2}] ){ x_{1} ↦ εx_{1}. ¬^{Q_{1}}G_{1}[Q_{2}x_{2}. G_{2}] }. (F_{2})

If we rewrite the outermost redex in F_{1}, we obtain the formula

( G_{1}[G_{2}{x_{2} ↦ εx_{2}. ¬^{Q_{2}}G_{2}}] )σ

written with the help of the substitution σ given as

{ x_{1} ↦ εx_{1}. ¬^{Q_{1}}G_{1}[G_{2}{x_{2} ↦ εx_{2}. ¬^{Q_{2}}G_{2}}] }. (σ)

If we propagate this substitution, by Corollary 2.5 we obtain a formula given by the context

G_{1}σ[⋯] (C)

where we read the dots “⋯” as

(G_{2}{x_{2} ↦ εx_{2}. ¬^{Q_{2}}G_{2}})σ.

Because x_{2} occurs free in none of dom(σ), G_{1}[⋯], G_{1}[G_{2}{x_{2} ↦ εx_{2}. ¬^{Q_{2}}G_{2}}], ran(σ), by Corollary 2.4 we can propagate σ further to write the inner formula as

G_{2}σ{x_{2} ↦ εx_{2}. ¬^{Q_{2}}G_{2}σ}. (I)

Putting (C) and (I) together again, we can choose formula F_{4} with the property F_{1}⟶F_{4}

as follows: G_{1}σ[ G_{2}σ{x_{2} ↦ εx_{2}. ¬^{Q_{2}}G_{2}σ} ]. (F_{4})

If we now rewrite all occurrences of the redex mentioned at the end of the notation of the formula F_{2} in parallel, then we obtain the formula

( G_{1}[Q_{2}x_{2}. G_{2}] )σ.

Before we can rewrite the remaining redex, we have to propagate σ to obtain a clear description of it. By Corollary 2.5, this results again in a context as given in (C) above, where, however, we now read the “⋯” as

Q_{2}x_{2}. G_{2}σ.

Note that, in this formula, the substitution σ has passed the quantifier “Q_{2}x_{2}.” soundly. Indeed, as mentioned above, x_{1} is different from x_{2}, and x_{2} cannot occur free in ran(σ). Putting this formula and its context together again, we can choose as F_{3} with the property

F_{3}⟵ ∥ F_{2} as follows: G_{1}σ[ Q_{2}x_{2}. G_{2}σ ]. (F_{3})

If we now rewrite the remaining redex, we again obtain the formula F_{4}, as was to be shown for item 1.

For item 2, it suffices to note that, if x_{2} occurs free in G_{2}, then x_{2} also occurs free in G_{2}σ because x_{1} and x_{2} are different.

For item 3, it suffices to note that, if x_{1} occurs free in G_{1}[Q_{2}x_{2}. G_{2}], then x_{1} also occurs free in G_{1}[G_{2}{x_{2} ↦ εx_{2}. ¬^{Q_{2}}G_{2}}].

For item 4, it suffices to note that, if x_{1} does not occur free in G_{1}[Q_{2}x_{2}. G_{2}], then both F_{2} and F_{3} are actually G_{1}[Q_{2}x_{2}. G_{2}]. Q.e.d. (Lemma 3.3)

As overlaps are trivial and as peaks of local divergence with parallel redexes are joinable in one step at each side trivially, we get as a corollaries of Lemma 3.3(1,4) and Corollary 3.2:

Corollary 3.4 ⟶ is locally confluent.

Corollary 3.5 For all F_{1}, F_{2} with F_{1}⟵ ∘ ⟶_{0}F_{2}, we have F_{1}⟶^{+} ∘ ⟵ F_{2}.

3.2 Well-Foundedness

As every ⟶_{0}-step (vacuous quantifiers) and every ⟶_{I}-step (innermost quantifiers) reduces the number occurrences of quantifiers by 1, we have:

Corollary 3.6 ⟵_{0} ∪ ⟵_{I} is well-founded.

Theorem 3.7 ⟵ is well-founded.

Proof of Theorem 3.7

Assume that B is a non-empty class. Then there is some a ∈ B. We just have to find an ⟵-minimal element in B.

If a is ⟵-minimal in B, then we have succeeded. Thus suppose that a is not ⟵-minimal in B. Then a ∈ dom(⟶).

Set A := ⟨{a}⟩⟶^{∗}. Set ⟶_{4} := _{A}↿⟶. It now suffices to show that ⟵_{4} is well-founded (because an ⟵_{4}-minimal element of A ∩ B is also an ⟵-minimal element of B).

By Corollary 3.6, A has an ⟵_{I}-minimal element a′. As a′ ∉ dom(⟶) by Corollary 3.1, a′ is an ⟶-normal form of a. To obtain the well-foundedness of ⟵_{4}, we are now going to apply Theorem 2.2.

Set ⟶_{2} := ⟶^{∗}_{0} ∘ ⟶_{1}. Set ⟶_{3} := ⟶_{0} ∪ ⟶_{1}. Then ⟶ = ⟶_{3}.

It now suffices to show items 1 to 4 of Theorem 2.2. Item 1 holds by Corollary 3.6. Item 3 holds by Corollary 3.4. Item 4 holds by Corollary 3.5. As the number of occurrences of the ε is invariant under ⟶_{0} and is increased at least by 1 by every ⟶_{1}-step, it increases at least by 1 by every ⟶_{2}-step. Thus, to satisfy item 2, we can choose the upper bound n to be the number of occurrences of ε in a′ (minus the number in a). Q.e.d. (Theorem 3.7)

3.3 Confluence

By the Newman Lemma (cf. [Newman, 1942] or, for a formal proof, [Wirth, 2004, § 3.4]), we obtain from Corollary 3.4 and Theorem 3.7:

Theorem 3.8 ⟶ is confluent.

3.4 On the Length of Derivations

By Theorems 3.7 and 3.8, we now know for certain that the rewrite relation is confluent and terminating (as its reverse is even well-founded), which means that we can eliminate the quantifiers in any order — but this does not mean that this is efficient.

Here is a serious warning to the contrary: The nesting depth of the occurrences of the εsymbols introduced by the normalization can be exponential in the number of quantifiers in the input formula, and the number of steps of an outermost normalization is even higher and seems to be non-elementary, cf. [Wirth, 2015, Example 4.7], [Wirth, 2008, Example 8].

As any innermost rewrite step reduces the number of quantifiers exactly by 1, and as no rewrite step can reduce the number of quantifiers by more than 1, we immediately get:

Theorem 3.9 Let F be a formula with n quantifiers. Innermost rewriting of F by ⟶_{I} obtains the (unique) ⟶-normal form F′ of F in exactly n steps, which is the minimal number of steps to reach F′ by ⟶ from F.

4 Conclusion

With Theorems 3.7 and 3.8, we have shown confluence and termination of the elimination of quantifiers via their explicit definition via Hilbert’s ε. This means in particular that any first-order term with quantifiers and epsilons (and formula variables), has a unique normal form w.r.t. this elimination of quantifiers, which has its first explicit occurrence in [Hilbert & Bernays, 1939], namely in the proof of the 1^{st} ε-theorem on Page 19f.

Moreover, the directness, self-containedness, and easy verifiability of the proofs should settle the questions on confluence and termination here once and for all — at least for working mathematicians. Formalists and rewriters, however, may see the need to develop a more formal verification of our proof and write a short paper that our results are all trivial in some higher-order rewriting theory. Writing or helping to find a good textbook on higher-order rewriting, however, seems to be in more urgent demand.

Furthermore, we hope that some philosophers will be stimulated by this paper to pick up the subject of the non-triviality of higher-order explicit definition and write or help to find a book on that subject.

Finally, the starting point of our interest in the subject, namely the question whether there is a lacuna in Hilbert–Bernays as discussed in § 1.3, needs further discussion by the experts on Hilbert’s ε and the history of mathematical logic in the 20^{th} century. On basis of our current knowledge, we would clearly answer this question positively.

References

[Ackermann, 1925] Wilhelm Ackermann, 1925. Begründung des ”tertium non datur“ mittels der Hilbertschen Theorie der Widerspruchsfreiheit. Mathematische Annalen, 93:1–36. Received March 30, 1924. Inauguraldissertation, 1924, Göttingen.

[Anon, 1899] Anon, editor, 1899. Festschrift zur Feier der Enthüllung des Gausz-Weber-Denkmals in Göttingen, herausgegeben von dem Fest-Comitee. Verlag von B. G. Teubner, Leipzig.

[Codish & Middeldorp, 2004] Michael Codish and Aart Middeldorp, 2004. 7^{th} Int. Workshop on Termination (WST), 2004. Technical Report AIB–2004–07, RWTH Aachen, Dept. of Computer Sci.. ISSN 0935–3232. http://sunsite.informatik.

rwth-aachen.de/Publications/AIB/2004/2004-07.ps.gz.

[Gillman, 1987] Leonard Gillman, 1987. Writing Mathematics Well. The Mathematical Association of America.

[Heijenoort, 1971] Jean van Heijenoort, 1971. From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Harvard Univ. Press. 2^{nd} rev. edn. (1^{st} edn. 1967).

[Hilbert, 1899] David Hilbert, 1899. Grundlagen der Geometrie. In [Anon, 1899, pp. 1– 92]. 1^{st} edn. without appendixes. Reprinted in [Hilbert, 2004, pp. 436–525]. (Last edition of “Grundlagen der Geometrie” by Hilbert is [Hilbert, 1930b], which is also most complete regarding the appendixes. Last three editions by Paul Bernays are [Hilbert, 1962; 1968; 1972], which are also most complete regarding supplements and figures. Its first appearance as a separate book was the French translation [Hilbert, 1900b]. Two substantially different English translations are [Hilbert, 1902] and [Hilbert, 1971]).

[Hilbert, 1900a] David Hilbert, 1900a. Über den Zahlbegriff. Jahresbericht der Deutschen Mathematiker-Vereinigung, 8:180–184. Received Dec. 1899. Reprinted as Appendix VI of [Hilbert, 1909; 1913; 1922; 1923; 1930b].

[Hilbert, 1900b] David Hilbert, 1900b. Les principes fondamentaux de la géométrie. Annales Scientifiques de l’École Normale Supérieure, Série 3, 17:103–209. French translation by Léonce Laugel of special version of [Hilbert, 1899], revised and authorized by Hilbert. Also in published as a separate book by the same publisher (Gauthier-Villars, Paris).

[Hilbert, 1902] David Hilbert, 1902. The Foundations of Geometry. Open Court, Chicago. English translation by E. J. Townsend of special version of [Hilbert, 1899], revised

and authorized by Hilbert, http://www.gutenberg.org/etext/17384.

[Hilbert, 1903] David Hilbert, 1903. Grundlagen der Geometrie. — Zweite, durch Zusätze vermehrte und mit fünf Anhängen versehene Auflage. Mit zahlreichen in den Text gedruckten Figuren. Druck und Verlag von B. G. Teubner, Leipzig. 2^{nd} rev. extd. edn. of [Hilbert, 1899], rev. and extd. with five appendixes, newly added

figures, and an index of notion names.

[Hilbert, 1905] David Hilbert, 1905. Über die Grundlagen der Logik und der Arithmetik. In [Krazer, 1905, pp. 174–185]. Reprinted as Appendix VII of [Hilbert, 1909; 1913; 1922; 1923; 1930b]. English translation On the foundations of logic and arithmetic by Beverly Woodward with an introduction by Jean van Heijenoort in [Heijenoort, 1971, pp. 129–138].

[Hilbert, 1909] David Hilbert, 1909. Grundlagen der Geometrie. — Dritte, durch Zusätze und Literaturhinweise von neuem vermehrte und mit sieben Anhängen versehene Auflage. Mit zahlreichen in den Text gedruckten Figuren. Number VII in Wissenschaft und Hypothese. Druck und Verlag von B. G. Teubner, Leipzig, Berlin. 3^{rd} rev. extd. edn. of [Hilbert, 1899], rev. edn. of [Hilbert, 1903], extd. with a bibliography and two additional appendixes (now seven in total) (Appendix VI: [Hilbert, 1900a]) (Appendix VII: [Hilbert, 1905]).

[Hilbert, 1913] David Hilbert, 1913. Grundlagen der Geometrie. — Vierte, durch Zusätze und Literaturhinweise von neuem vermehrte und mit sieben Anhängen versehene Auflage. Mit zahlreichen in den Text gedruckten Figuren. Druck und Verlag von B. G. Teubner, Leipzig, Berlin. 4^{th} rev. extd. edn. of [Hilbert, 1899], rev. edn. of [Hilbert, 1909].

[Hilbert, 1922] David Hilbert, 1922. Grundlagen der Geometrie. — Fünfte, durch Zusätze und Literaturhinweise von neuem vermehrte und mit sieben Anhängen versehene Auflage. Mit zahlreichen in den Text gedruckten Figuren. Verlag und Druck von B. G. Teubner, Leipzig, Berlin. 5^{th} extd. edn. of [Hilbert, 1899]. Contrary to what the sub-title may suggest, this is an anastatic reprint of [Hilbert, 1913], extended by a very short preface on the changes w.r.t. [Hilbert, 1913], and with augmentations to Appendix II, Appendix III, and Chapter IV, § 21.

[Hilbert, 1923] David Hilbert, 1923. Grundlagen der Geometrie. — Sechste unveränderte Auflage. Anastatischer Nachdruck. Mit zahlreichen in den Text gedruckten Figuren. Verlag und Druck von B. G. Teubner, Leipzig, Berlin. 6^{th} rev. extd. edn. of [Hilbert, 1899], anastatic reprint of [Hilbert, 1922].

[Hilbert, 1926] David Hilbert, 1926. Über das Unendliche — Vortrag, gehalten am 4. Juni 1925 gelegentlich einer zur Ehrung des Andenkens an Weierstrasz von der Westfälischen Math. Ges. veranstalteten Mathematiker-Zusammenkunft in Münster i. W. Mathematische Annalen, 95:161–190. Received June 24, 1925. Reprinted as Appendix VIII of [Hilbert, 1930b]. English translation On the infinite by Stefan Bauer-Mengelberg with an introduction by Jean van Heijenoort in [Heijenoort, 1971, pp. 367–392].

[Hilbert, 1928] David Hilbert, 1928. Die Grundlagen der Mathematik — Vortrag, gehalten auf Einladung des Mathematischen Seminars im Juli 1927 in Hamburg. Abhandlungen aus dem mathematischen Seminar der Univ. Hamburg, 6:65–85. Reprinted as Appendix IX of [Hilbert, 1930b]. English translation The foundations of mathematics by Stefan Bauer-Mengelberg and Dagfinn Føllesdal with a short introduction by Jean van Heijenoort in [Heijenoort, 1971, pp. 464–479].

[Hilbert, 1930a] David Hilbert, 1930a. Probleme der Grundlegung der Mathematik. Mathematische Annalen, 102:1–9. Vortrag gehalten auf dem Internationalen Mathematiker-Kongreß in Bologna, Sept. 3, 1928. Received March 25, 1929. Reprinted as Appendix X of [Hilbert, 1930b]. Short version in Atti del congresso internationale dei matematici, Bologna, 3–10 settembre 1928, Vol. 1, pp. 135–141, Bologna, 1929.

[Hilbert, 1930b] David Hilbert, 1930b. Grundlagen der Geometrie. — Siebente umgearbeitete und vermehrte Auflage. Mit 100 in den Text gedruckten Figuren. Verlag und Druck von B. G. Teubner, Leipzig, Berlin. 7^{th} rev. extd. edn. of [Hilbert, 1899], thoroughly revised edition of [Hilbert, 1923], extd. with three new appendixes (now ten in total) (Appendix VIII: [Hilbert, 1926]) (Appendix IX: [Hilbert, 1928]) (Appendix X: [Hilbert, 1930a]).

[Hilbert, 1956] David Hilbert, 1956. Grundlagen der Geometrie. — Achte Auflage, mit Revisionen und Ergänzungen von Dr. Paul Bernays. Mit 124 Abbildungen. B. G. Teubner Verlagsgesellschaft, Stuttgart. 8^{th} rev. extd. edn. of [Hilbert, 1899], rev. edn. of [Hilbert, 1930b], omitting appendixes VI–X, extd. by Paul Bernays, now with 24 additional figures and 3 additional supplements.

[Hilbert, 1962] David Hilbert, 1962. Grundlagen der Geometrie. — Neunte Auflage, revidiert und ergänzt von Dr. Paul Bernays. Mit 129 Abbildungen. B. G. Teubner Verlagsgesellschaft, Stuttgart. 9^{th} rev. extd. edn. of [Hilbert, 1899], rev. edn. of [Hilbert, 1956], extd. by Paul Bernays, now with 129 figures, 5 appendixes, and 8 supplements (I 1, I 2, II, III, IV 1, IV 2, V 1, V 2).

[Hilbert, 1968] David Hilbert, 1968. Grundlagen der Geometrie. — Zehnte Auflage, revidiert und ergänzt von Dr. Paul Bernays. Mit 124 Abbildungen. B. G. Teubner Verlagsgesellschaft, Stuttgart. 10^{th} rev. extd. edn. of [Hilbert, 1899], rev. edn. of [Hilbert, 1962] by Paul Bernays.

[Hilbert, 1971] David Hilbert, 1971. The Foundations of Geometry. Open Court, Chicago and La Salle (IL). Newly translated and fundamentally different 2^{nd} edn. of [Hilbert, 1902], actually an English translation of [Hilbert, 1968] by Leo Unger.

[Hilbert, 1972] David Hilbert, 1972. Grundlagen der Geometrie. — 11. Auflage. Mit Supplementen von Dr. Paul Bernays. B. G. Teubner Verlagsgesellschaft, Stuttgart. 11^{th} rev. extd. edn. of [Hilbert, 1899], rev. edn. of [Hilbert, 1968] by Paul Bernays.

[Hilbert, 2004] David Hilbert, 2004. David Hilbert’s Lectures on the Foundations of Geometry, 1891–1902. Springer. Ed. by Michael Hallett and Ulrich Majer.

[Hilbert & Bernays, 1934] David Hilbert and Paul Bernays, 1934. Grundlagen der Mathematik — Erster Band. Number XL in Grundlehren der mathematischen Wissenschaften. Springer. 1^{st} edn. (2^{nd} edn. is [Hilbert & Bernays, 1968]). Reprinted by J. W. Edwards Publ., Ann Arbor (MI), 1944. English translation is [Hilbert & Bernays, 2016a; 2016b].

[Hilbert & Bernays, 1939] David Hilbert and Paul Bernays, 1939. Grundlagen der Mathematik — Zweiter Band. Number L in Grundlehren der mathematischen Wissenschaften. Springer. 1^{st} edn. (2^{nd} edn. is [Hilbert & Bernays, 1970]). Reprinted by J. W. Edwards Publ., Ann Arbor (MI), 1944.

[Hilbert & Bernays, 1968] David Hilbert and Paul Bernays, 1968. Grundlagen der Mathematik I. Number 40 in Grundlehren der mathematischen Wissenschaften. Springer. 2^{nd} rev. edn. of [Hilbert & Bernays, 1934]. English translation is [Hilbert & Bernays, 2016a; 2016b].

[Hilbert & Bernays, 1970] David Hilbert and Paul Bernays, 1970. Grundlagen der Mathematik II. Number 50 in Grundlehren der mathematischen Wissenschaften. Springer. 2^{nd} rev. extd. edn. of [Hilbert & Bernays, 1939].

[Hilbert & Bernays, 2016a] David Hilbert and Paul Bernays, 2016a. Grundlagen der Mathematik I — Foundations of Mathematics I, Part A: Title Pages, Prefaces, and §§ 1–2. Springer. First English translation and bilingual facsimile edn. of the 2^{nd} German edn. [Hilbert & Bernays, 1968], incl. the annotation and translation of all differences of the 1^{st} German edn. [Hilbert & Bernays, 1934]. Ed. by Claus-Peter Wirth, Jörg Siekmann, Volker Peckhaus, Michael Gabbay, Dov Gabbay. Translated and commented by Claus-Peter Wirth &al. Thoroughly rev. 3^{rd} edn. (1^{st} edn. College Publications, London, 2011; 2^{nd} edn. http://wirth.

bplaced.net/p/hilbertbernays, 2013).

[Hilbert & Bernays, 2016b] David Hilbert and Paul Bernays, 2016b. Grundlagen der Mathematik I — Foundations of Mathematics I, Part B: §§ 3–5 and Deleted Part I of the 1^{st} Edn.. Springer. First English translation and bilingual facsimile edn. of the 2^{nd} German edn. [Hilbert & Bernays, 1968], incl. the annotation and translation of all deleted texts of the 1^{st} German edn. [Hilbert & Bernays, 1934]. Ed. by Claus-Peter Wirth, Jörg Siekmann, Volker Peckhaus, Michael Gabbay, Dov Gabbay. Translated and commented by Claus-Peter Wirth &al. Thoroughly rev. 3^{rd} edn. (1^{st} edn. College Publications, London, 2012; 2^{nd} edn. http://wirth.

bplaced.net/p/hilbertbernays, 2013).

[Jouannaud & Okada, 1991] Jean-Pierre Jouannaud and Mitsuhiro Okada, 1991. A computation-model for executable higher-order algebraic specification languages. In [LICS, 1991, pp. 350–361].

[Ketema & Raamsdonk, 2004] Jeroen Ketema and Femke van Raamsdonk, 2004. Erasure and termination in higher-order rewriting. In [Codish & Middeldorp, 2004,

pp. 30–33]. Also available at www.prove-and-die.org/publ/wst04.pdf.

[Klop, 1980] Jan Willem Klop, 1980. Combinatory reduction systems. Mathematical centre tracts 127, Mathematisch Centrum (since 1983: Centrum Wiskunde & Informatica), Amsterdam. PhD thesis, Utrecht Univ.., http://libgen.io/get.php?md5=

a80df1dda74dffd97700bda2277e8bc4.

[Klop &al., 1993] Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk, 1993. Combinatory reduction systems: introduction and survey. Theoretical Computer Sci., 121:279–308.

[Krazer, 1905] A. Krazer, editor, 1905. Verhandlungen des Dritten Internationalen Mathematiker-Kongresses, Heidelberg, Aug. 8–13, 1904. Verlag von B. G. Teubner, Leipzig.

[LICS, 1991] LICS, 1991. Proc. 6^{th} Annual IEEE Symposium on Logic In Computer Sci. (LICS), Amsterdam, 1991. IEEE Press. http://lii.rwth-aachen.de/lics/

archive/1991.

[Middeldorp, 2001] Aart Middeldorp, editor, 2001. 12^{th} Int. Conf. on Rewriting Techniques and Applications (RTA), Utrecht (The Netherlands), 2001, number 2051 in Lecture Notes in Computer Science. Springer.

[Moore & Wirth, 2014] J Strother Moore and Claus-Peter Wirth, 2014. Automation of Mathematical Induction as part of the History of Logic. SEKI-Report SR–2013–02 (ISSN 1437–4447). SEKI Publications. Rev. edn. July 2014 (1^{st} edn. 2013), ii+107 pp.,

http://arxiv.org/abs/1309.6226.

[Narendran & Rusinowitch, 1999] Paliath Narendran and Michaël Rusinowitch, editors, 1999. 10^{th} Int. Conf. on Rewriting Techniques and Applications (RTA), Trento (Italy), 1999, number 1631 in Lecture Notes in Computer Science. Springer.

[Newman, 1942] Max H. A. Newman, 1942. On theories with a combinatorial definition of equivalence. Annals of Mathematics, 43:223–242.

[Nipkow, 1991] Tobias Nipkow, 1991. Higher-order critical pairs. In [LICS, 1991, pp. 342– 349].

[Raamsdonk, 1999] Femke van Raamsdonk, 1999. Higher-order rewriting. In [Narendran & Rusinowitch, 1999, pp. 221–239].

[Raamsdonk, 2001] Femke van Raamsdonk, 2001. On termination of higher-order rewriting. In [Middeldorp, 2001, pp. 261–275].

[Raamsdonk, 2013] Femke van Raamsdonk, editor, 2013. 24^{th} Int. Conf. on Rewriting Techniques and Applications (RTA), Einhoven (The Netherlands), 2013, number 24 in Leibniz Int. Proc. in Informatics. Dagstuhl (Germany).

[Tait, 1967] William W. Tait, 1967. Intensional interpretations of functionals of finite type I. J. Symbolic Logic, 32:198–212.

[Winkler &al., 2013] Sarah Winkler, Harald Zankl, and Aart Middeldorp, 2013. Beyond Peano Arithmetic — automatically proving termination of the Goodstein

sequence. In [Raamsdonk, 2013, pp. 335–351].

[Wirth, 2004] Claus-Peter Wirth, 2004. Descente Infinie + Deduction. Logic J. of the

IGPL, 12:1–96. http://wirth.bplaced.net/p/d.

[Wirth, 2008] Claus-Peter Wirth, 2008. Hilbert’s epsilon as an operator of indefinite committed choice. J. Applied Logic, 6:287–317. http://dx.doi.org/10.1016/j.

jal.2007.07.009.

[Wirth, 2009] Claus-Peter Wirth, 2009. Shallow confluence of conditional term rewriting systems. J. Symbolic Computation, 44:69–98. http://dx.doi.org/10.1016/j.jsc.

2008.05.005.

[Wirth, 2015] Claus-Peter Wirth, 2015. A Simplified and Improved Free-Variable Framework for Hilbert’s epsilon as an Operator of Indefinite Committed Choice. SEKI Report SR–2011–01 (ISSN 1437–4447). SEKI Publications. Rev. edn. June 2015

(1^{st} edn. 2011), ii+82 pp., http://arxiv.org/abs/1104.2444.