{'fraction_non_alphanumeric': 0.07638983901126466, 'fraction_numerical': 0.006612851735303507, 'mean_word_length': 3.304672163329407, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 23, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Semantics and Proof Theory of the Epsilon Calculus

The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the epsilon-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic interpretations. The problems facing the development of proof-theoretically well-behaved systems are outlined.

have been investigated by Blass and Gurevich [6]. These different semantics result in different expressive power (in particular, over finite models), and are characterized by different formalizations. Below we present the first two versions of the semantics of the ε-calculus and sketch completeness results.
The very beginnings of proof theory in the work of Hilbert and his students consisted in the proof theoretic study of axiom systems for the ε-calculus. One of the most significant results in this connection are the epsilon theorems. It plays a role similar to Gentzen's midsequent theorem in the proof theory of the sequent calculus: it yields a version of Herbrand's Theorem. In fact, it was used to give the first correct proof of Herbrand's theorem (Hilbert and Bernays [11]). In a simple formulation, the theorem states that if an existential formula (∃x)A(x) (not containing ε) is derivable in the epsilon calculus, then there are terms t 1 , . . . , t n so that a (Herbrand-) disjunction A(t 1 ) ∨ . . . ∨ A(t n ) is derivable in propositional logic. The proof gives a constructive procedure that, given a derivation of (∃x)A(x), produces the corresponding Herbrand disjunction. An analysis of this proof (see [18]) gives a hyper-exponential bound on the length of the Herbrand disjunction in the number of critical formulas occurring in the proof. The bound is essentially optimal, since it is known from work by Orevkov and Statman that the length of Herbrand disjunctions is hyper-exponential in the length of proofs of the original existential formula (this is the basis for familiar speed-up theorems of systems with cut over cut-free systems). In section 4 we prove the first epsilon theorem with identity, along the lines of Bernays's proof.
A general proof theory of the epsilon calculus requires formal systems that are more amenable to proof-theoretic investigations than the Hilbert-type axiomatic systems studied in the Hilbert school. Although some sequent systems for the epsilon calculus exist, it is not clear that they are the best possible formulations, nor have their proof-theoretic properties been investigated in depth. Maehara's [13] and Leisenring's [12] systems were not cut-free complete. Yasuhara [21] studied a cut-free complete system, but only gave a semantic cut-elimination proof. Section 5 surveys these and other systems, and highlights some of the difficulties in developing a systematic proof theory on the basis of them. Proof-theoretically suitable formalisms for the ε-calculus are still a desideratum for applications of the epsilon calculus.
The classical ε-calculus is usually investigated as a proof-theoretic formalism, and no systematic study of the model theory of epsilon calculi other than Asser's classic [3] exists. However, Abiteboul and Vianu [2], Blass and Gurevich [6], and Otto [19] have studied the model theory of choice operators in the context of finite model theory and database query languages. And applications of choice operators to model definite and indefinite noun phrases in computational linguistics Meyer Viol [15] and von Heusinger [8,9] have led to the definition of indexed epsilon calculus by Mints and Sarenac [16].
With a view to applications, it is especially important to develop the semantics and proof theory of epsilon operators in non-classical logics. Of particular importance in this context is the development of epsilon calculi for intuitionistic logic, not least because this is the context in which the epsilon calculus can and has been applied in programming language semantics. Some work has been done on intuitionistic ε-calculi (e.g., Bell [5], DeVidi [7], Meyer Viol [15], Mints [17]), but there are still many important open questions. The straightforward extensions of intuitionistic logic by epsilon operators are not conservative and result in intermediate logics related to Gödel logic. Meyer Viol [15] has proposed a conservative extensions of intuitionistic logic by epsilon operators which warrants further study.

Syntax and Axiomatic Proof Systems
Definition 1. The language of of the elementary calculus L = EC contains the usual logical symbols (variables, function and predicate symbols, =). A subscript ε will indicate the presence of the symbol ε, and ∀ the presence of the quantifiers ∀ and ∃. The terms Trm and formulas Frm of L ε∀ are defined as usual, but simultaneously, to include: If A is a formula in which x has a free occurrence but no bound occurrence, then ε x A is a term, and all occurrences of x in it are bound.
If E is an expression (term or formula), then FV(E) is the set of variables which have free occurrences in E.
When E, E ′ are expressions (terms or formulas), we write E ≡ E ′ iff E and E ′ are syntactically identical up to a renaming of bound variables. We say that a term t is free for x in E iff x does not occur free in the scope of an ε-operator ε y or quantifier ∀y, ∃y for any y ∈ FV(t).
If E is an expression and t is a term, we write E[x/t] for the result of substituting every free occurrence of x in E by t, provided t is free for x in E, and renaming bound variables in t if necessary. We write E(x) to indicate that x ∈ FV(E), and E(t) for E[x/t]. We write E{t/u} for the result of replacing every occurrence of t in E by u. 1 Definition 2 (ε-Translation). If E is an expression, define E ε by: 1 Skipping details, (a) we want to replace not just every occurrence of t by u, but every occurrence of a term t ′ ≡ t. (b) t may have an occurrence in E where a variable in t is bound by a quantifier or ε outside t, and such occurrences shouldn't be replaced (they are not subterm occurrences). (c) When replacing t by u, bound variables in u might have to be renamed to avoid conflicts with the bound variables in E ′ and bound variables in E ′ might have to be renamed to avoid free variables in u being bound. Note that if e is subordinate to e ′ it is not a subterm of e ′ , because x is free in e and so the occurrence of e (really, of the variant e ′′ ) in e ′ is in the scope of ε x . 2 Definition 8. The rank rk(e) of an ε-term e is defined as follows: (1) rk(e) = 1 iff e contains no subordinate ε-terms. (2) rk(e) = max{rk(e 1 ), . . . , rk(e n )} + 1 if e 1 , . . . , e n are all the ε-terms subordinate to e. Proposition 9. If p is the type of e, then rk(p) = rk(e). and its only rule of inference is

Axioms and Proofs
The axioms and rules of the (intensional) ε-calculus EC ε (EC = ε ) are those of EC (EC = ) plus the critical formulas (crit) The axioms and rules of the extensional ε-calculus EC ext ε are those of EC = ε plus The axioms and rules of EC ∀ , EC ε∀ , EC ext ε∀ are those of EC, EC ε , EC ext ε , respectively, together with the axioms and the rules Applications of these rules must satisfy the eigenvariable condition, viz., the variable x must not appear in the conclusion or anywhere below it in the proof.
Definition 11. If Γ is a set of formulas, a proof of A from Γ in EC ext ε∀ is a sequence π of formulas A 1 , . . . , A n = A where for each i ≤ n, A i ∈ Γ , A i is an instance of an axiom, or follows from formulas A j (j < i) by a rule of inference.
If π only uses the axioms and rules of EC, EC ε , EC ext ε , etc., then it is a proof of A from Γ in EC, EC ε , EC ext ε , etc., and we write Γ ⊢ π A, Γ ⊢ π ε A, Γ ⊢ π εext A, etc. We Note that our definition of proof, because of its use of ≡, includes a tacit rule for renaming bound variables. Note also that substitution into members of Γ is not permitted. However, we can simulate a provability relation in which substitution into members of Γ is allowed by considering Γ inst , the set of all substitution instances of members of Γ . If Γ is a set of sentences, then Γ inst = Γ .
Proof. By induction on the length of π, as in the classical case.
Proof. Suppose Γ, Φ, s |= Γ . We show by induction on the length n of a proof π that M, Φ, s ′ |= A for all s ′ which agree with s on FV(Γ ). We may assume that no eigenvariable x of π is in FV(Γ ) (if it is, let y / ∈ FV(π) and not occurring in π; consider π[x/y] instead of π).
If n = 0 there's nothing to prove. Otherwise, we distinguish cases according to the last line A n in π. The only interesting case is when A n is a critical formula, Lemma 29. If Γ is a set of sentences and Γ ⊢ ε ⊥, then there are M, Φ so that M, Φ |= Γ .
The proof of the Lemma comes in several stages. We have to show that if Γ is consistent, we can construct M, Φ, and s so that M, Φ, s |= Γ . Since FV(Γ ) = ∅, we then have M, Φ |= Γ . (1), observe that if Γ * ⊢ π ε ⊥, then π contains only finitely many formulas from Γ * , so for some n, Γ n ⊢ π ε ⊥. But Γ n is consistent by definition.
Definition 33. Let ≈ be the relation on Trm ε defined by t ≈ u iff t = u ∈ Γ * It is easily seen that ≈ is an equivalence relation. Let t = {u : u ≈ t} and Trm = { t : t ∈ Trm}.
Let Φ 0 be a fixed choice function on Trm, and define Proof. We show that val M,Φ,s (t) = t and M, Φ, s |= A iff A ∈ Γ * by simultaneous induction on the complexity of t and A.
If t = c is a constant, the claim holds by definition of (·) M . If A = ⊥ or = ⊤, the claim holds by Lemma 32.

Semantics for EC ε
In order to give a complete semantics for EC ε , i.e., for the calculus without the extensionality axiom (ext), it is necessary to change the notion of choice function so that two ε-terms ε x A(x) and ε x B(x) may be assigned different representatives even when M, Φ, s |= ∀x(A(x) ↔ B(x)), since then the negation of (ext) is consistent in the resulting calculus. The idea is to add the ε-term itself as an additional argument to the choice function. However, in order for this semantics to be sound for the calculus-specifically, in order for (= 2 ) to be valid-we have to use not ε-terms but ε-types.
Definition 38. If M is a structure, Ψ an intensional choice operator, and s an assignment, val M,Ψ,s (t) and M, Ψ, s |= A is defined as before, except (6) in Definition 20 is replaced by: The soundness and completeness proofs generalize to EC ε , EC = ε , and EC ε∀ .

The Case Without Identity
Definition 39. An ε-term e is critical in π if A(t) → A(e) is one of the critical formulas in π. The rank rk(π) of a proof π is the maximal rank of its critical ε-terms. The r-degree deg(π, r) of π is the maximum degree of its critical ε-terms of rank r. The r-order o(π, r) of π is the number of different (up to renaming of bound variables) critical ε-terms of rank r.
Lemma 40. If e = ε x A(x), ε y B(y) are critical in π, rk(e) = rk(π), and B * ≡ B(u) → B(ε y B(y)) is a critical formula in π. Then, if e is a subterm of B * , it is a subterm of B(y) or a subterm of u.
Proof. Suppose not. Since e is a subterm of B * , we have B(y) ≡ B ′ (ε x A ′ (x, y), y) and either e ≡ ε x A ′ (x, u) or e ≡ ε x A ′ (x, ε y B(y)). In each case, we see that ε x A ′ (x, y) and e have the same rank, since the latter is an instance of the former (and so have the same type). On the other hand, in either case, ε y B(y) would be ε y B ′ (ε x A ′ (x, y), y) and so would have a higher rank than ε x A ′ (x, y) as that ε-term is subordinate to it. This contradicts rk(e) = rk(π).
Lemma 41. Let e, B * be as in the lemma, and t be any term. Then Lemma 42. If ⊢ π ε E and E does not contain ε, then there is a proof π ′ such that ⊢ π ′ ε E and rk(π ′ ) ≤ rk(pi) = r and o(π ′ , r) < o(π, r). Proof. Let e be an ε-term critical in π and let A(t 1 ) → A(e), dots, A(t n ) → A(e) be all its critical formulas in π.
Consider π{e/t} i , i.e., π with e replaced by t i throughout. Each critical formula belonging to e now is of the form A(t ′ j ) → A(t i ), since e obviously cannot be a subterm of A(x) (if it were, e would be a subterm of ε x A(x), i.e., of itself!). Letπ i be the sequence of tautologies A(t i ) → (A(t ′ j ) → A(t i )) for i = 1, . . . , n, followed by π{e/t} i . Each one of the formulas A(t ′ j ) → A(t i ) follows from one of these by (MP) from A(t i ). Hence, The ε-term e is not critical in π i : Its original critical formulas are replaced by , which are tautologies. By (1) of the preceding Lemma, no critical ε-term of rank r was changed at all. By (2) of the preceding Lemma, no critical ε-term of rank < r was replaced by a critical ε-term of rank ≥ r. Hence, o(π i , r) = o(π) − 1.
Let π ′′ be the sequence of tautologies ¬ n i=1 A(t i ) → (A(t i ) → A(e)) followed by π. Then n i=1 A(t i ) ⊢ π ′′ E , e is not critical in π ′′ , and otherwise π and π ′′ have the same critical formulas. The same goes for π ′′ [¬ A(t i )], a proof of We now obtain π ′ as the π i , i = 1, . . . , n, followed by π[¬ n i=1 A(t i )], followed by the tautology from which E follows by n + 1 applications of (MP).
Theorem 43 (First Epsilon Theorem for EC ε ). If E is a formula not containing any ε-terms and ⊢ ε E, then ⊢ ε E.
Corollary 44 (Extended First ε-Theorem). If ⊢ ε E(e 1 , . . . , e n ), then ⊢ m i=1 E(t j 1 , . . . , t j n ) for some terms t j (in EC). Proof. If E contains ε-terms, say, E is E(e 1 , . . . , e n ), then replacement of εterms in the construction of π i may change E-but of course only the ε-terms appearing as subterms in it. In each step we obtain not a proof of E but of some disjunction of instances E(e ′ 1 , . . . , e ′ n ). For details, see [18].

The Case with Identity
In the presence of the identity (=) predicate in the language, things get a bit more complicated. The reason is that instances of the (= 2 ) axiom schema, may also contain ε-terms, and the replacement of an ε-term e by a term t i in the construction of π i may result in a formula which no longer is an instance of (= 2 ). For instance, suppose that t is a subterm of e = e ′ (t) and A(t) is of the form A ′ (e ′ (t)). Then the original axiom is which after replacing e = e ′ (t) by t i turns into So this must be avoided. In order to do this, we first observe that just as in the case of the predicate calculus, the instances of (= 2 ) can be derived from restricted instances. In the case of the predicate calculus, the restricted axioms are t = u → (P n (s 1 , . . . , t, . . . s n ) → P n (s 1 , . . . , u, . . . , s n ) (= ′ 2 ) t = u → f n (s 1 , . . . , t, . . . , s n ) = f n (s 1 , . . . , u, . . . , s n ) (= ′′ 2 ) to which we have to add the ε-identity axiom schema: where ε x A(x; x 1 , . . . , x n ) is an ε-type.
Proof. By induction. Now replacing every occurrence of e in an instance of (= ′ 2 ) or (= ′′ 2 )-where e obviously can only occur inside one of the terms t, u, s 1 , . . . , s n -results in a (different) instance of (= ′ 2 ) or (= ′′ 2 ). The same is true of (= ε ), provided that the e is neither ε x A(x; s 1 , . . . , t, . . . s n ) nor ε x A(x; s 1 , . . . , u, . . . s n ). This would be guaranteed if the type of e is not ε x A(x; x 1 , . . . , x n ), in particular, if the rank of e is higher than the rank of ε x A(x; x 1 , . . . , x n ). Moreover, the result of replacing e by t i in any such instance of (= ε ) results in an instance of (= ε ) which belongs to the same ε-type. Thus, in order for the proof of the first ε-theorem to work also when = and axioms (= 1 ), (= ′ 2 ), (= ′′ 2 ), and (= ε ) are present, it suffices to show that the instances of (= ε ) with ε-terms of rank rk(π) can be removed. Call an ε-term e special in π, if π contains an occurrence of t = u → e ′ = e as an instance of (= ε ).
Proof. The basic idea is simple: Suppose t = u → e ′ = e is an instance of (= ε ), with e ′ ≡ ε x A(x; s 1 , . . . , t, . . . s n ) and e ≡ ε x A(x; s 1 , . . . , u, . . . s n ). Replace e everywhere in the proof by e ′ . Then the instance of (= ε ) under consideration is removed, since it is now provable from e ′ = e ′ . This potentially interferes with critical formulas belonging to e, but this can also be fixed: we just have to show that by a judicious choice of e it can be done in such a way that the other (= ε ) axioms are still of the required form.
Let p = ε x A(x; x 1 , . . . , x n ) be an ε-type of rank rk(π), and let e 1 , . . . , e l be all the ε-terms of type p which have a corresponding instance of (= ε ) in π. Let T i be the set of all immediate subterms of e 1 , . . . , e l , in the same position as x i , i.e., the smallest set of terms so that if e i ≡ ε x A(x; t 1 , . . . , t n ), then t i ∈ T . Now let let T * be all instances of p with terms from T i substituted for the x i . Obviously, T and thus T * are finite (up to renaming of bound variables). Pick a strict order ≺ on T which respects degree, i.e., if deg(t) < deg(u) then t ≺ u.
If rk(e ′′ ) < rk(e), then the replacement of e by e ′ can only change subterms of e ′′ and e ′′′ . In this case, the uniform replacement results in another instance of (= ε ) with ε-terms of the same ε-type, and hence of the same rank < rk(π), as the original.
If rk(e ′′ ) = rk(e) but has a different type than e, then this axiom is unchanged in π 0 : Neither e ′′ nor e ′′′ can be ≡ e, because they have different ε-types, and neither e ′′ nor e ′′′ (nor t ′ or u ′ , which are subterms of e ′′ , e ′′′ ) can contain e as a subterm, since then e wouldn't be degree-maximal among the special ε-terms of π of rank rk(π).
If the type of e ′′ , e ′′′ is the same as that of e, e cannot be a proper subterm of e ′′ or e ′′′ , since otherwise e ′′ or e ′′′ would again be a special ε-term of rank rk(π) but of higher degree than e. So either e ≡ e ′′ or e ≡ e ′′′ , without loss of generality suppose e ≡ e ′′ . Then the (= ε ) axiom in question has the form which is no longer an instance of (= ε ), but can be proved from new instances of (= ε ). We have to distinguish two cases according to whether the indicated position of t and t ′ in e ′ , e ′′′ is the same or not. In the first case, u ≡ u ′ , and the new formula can be proved from t = u together with Since e ′ and e ′′′ already occurred in π, by assumption e ′ , e ′′′ ≺ e.
In the second case, the original formulas read, with terms indicated: and with e replaced by e ′ the latter becomes: This new formula is provable from t = u together with and some instances of (= ′ 2 ). Hence, π ′ contains a (possibly new) special εterm e ′′′′ . However, e ′′′′ ≺ e.
In the special case where e = e ′′ and e ′ = e ′′′ , i.e., the instance of (= ε ) we started with, then replacing e by e ′ results in t = u → e ′ = e ′ , which is provable from e ′ = e ′ , an instance of (= 1 ).
Let π 1 be π 0 with the necessary new instances of (= ε ), added. The instances of (= ε ) in π 1 satisfy the properties required in the statement of the lemma.
However, the results of replacing e by e ′ may have impacted some of the critical formulas in the original proof. For a critical formula to which e ≡ ε x A(x, u) belongs is of the form which after replacing e by e ′ becomes which is no longer a critical formula. This formula, however, can be derived from t = u together with Let π 2 be π 1 plus these derivations of (2) with the instances of (= 2 ) themselves proved from (= ′ 2 ) and (= ε ). The rank of the new critical formulas is the same, so the rank of π 2 is the same as that of π. The new instances of (= ε ) required for the derivation of the last two formulas only contain ε-terms of lower rank that that of e, as can be verified. π 2 is thus a proof of E from t = u which satisfies the conditions of the lemma. From it, we obtain a proof π 2 [t = u] of t = u → E by the deduction theorem. On the other hand, the instance t = u → e ′ = e under consideration can also be proved trivially from t = u. The proof π[t = u] thus is also a proof, this time of t = u → E, which satisfies the conditions of the lemma. We obtain π ′ by combining the two proofs.
Theorem 48 (First Epsilon Theorem for EC = ε ). If E is a formula not containing any ε-terms and ⊢ ε= E, then ⊢ = E (in EC = ).
Open Problem 49. Prove cut-elimination for the Mints-Yasuhara system, or give a similarly simple sequent calculus for which it can be proved.

Natural deduction
In Gentzen's classical natural deduction system NK, the quantifier rules are given by . . . .

C B ∃E
where z must not appear in any undischarged assumptions (nor in A(x) or B). Meyer Viol [15] has proposed a system in which the ∃E rule is replaced by ∃E ε and the following term rule is added Open Problem 50. Does Meyer Viol's system have a normal form theorem?
Adding ∃E ε and Iε to the intuitionistic system NJ results in a system that is not conservative over intuitionistic logic. For instance, Plato's principle, the formula ∃x(∃y A(y) → A(x)) becomes derivable: [∃y A(ε x A(x))] A(ε x A(x)) ∃E ε ∃y A(y) → A(ε x A(x)) → I ∃x(∃y A(y) → A(x)) ∃I However, the system also does not collapse to classical logic: it is conservative for propositional formulas. Intuitionistic natural deduction systems are especially intriguing, as Abadi, Gonthier and Werner [1] have shown that a system of quantified propositional intuitionistic logic with a choice operator ε X can be given a Curry-Howard correspondence via a type system which ε X A(X) is a type such that the type A(X) is inhabited. System E is paired with a simply typed λ-calculus that, in addition to λ-abstraction and application, features implementation: t : A with X = T of type A(ǫ X A/X). If A(X) is a type specification of an interface with variable type X, then A(T ) for some type T is an implementation of that interface.