Can adding Hilbert's epsilon to a theory, and then expanding that theories axiom schema to include the new language, cause it to become inconsistent?

Question

Epsilon Calculus is a formalism developed by Hilbert adding his $\epsilon$ operator to predicate logic. $\epsilon x. A(x)$ is a term such that $\exists x.A(x) \implies A(\epsilon x.A(x))$. In can actually replace the quantifiers, since $\exists x. A(x) \iff A(\epsilon x. A(x))$ and $\forall x. A(x) \iff A(\epsilon x.\lnot A(x))$. The second epsilon theorem states that if epsilon calculus proves epsilon calculus proves a statement in the language of predicate logic, so does predicate logic. This establishes its consistency. This theorem even if you enjoin it to other formal systems, like ZF or ZFC.

There is a caveat to that last statement though. In ZF, if you add the epsilon operator, and then add new axioms corresponding to the axiom schemas of specification and replacement, corresponding to the new formulas introduced by the $\epsilon$ operator, it actually becomes stronger than ZFC (but still equiconsistient to ZF). This corresponds roughly to the fact that for any nonempty set $S$, an element of $S$ is $\epsilon x.x \in S$, essentially introducing a global choice operator. You can only take advantage of this using the axiom schema of replacement.

Anyways, the point is that even though it significantly strengthens it, it is still equiconsistient. I'm wondering if this is always true?

Namely, for a language $L$ (which includes predicate logic) we will say that $A[\cdot]$ is an axiom schema is a formula in the language of $L$ with "holes" in it, where we can insert formulas. $A[F]$ (for example), would be $A[\cdot]$ with the holes filled with $F$. $A$ can also specify what variables are allowed to be free in its input.

For example, $\forall z. \exists S. \forall x. x \in S \iff \cdot \land x \in z$ is the axiom schema of specification. The input formula can have $z$ and $x$ free (but not $S$). (Actually, there are multiple axiom schema of replacements, corresponding to different number of "w" variables, according to this.)

The axiom schema of replacement is defined like wise. Also note that axioms are axiom schemas with $0$ holes.

A theory is a set of axiom schemas. If $X$ is a theory, then $X[S] := \{x[s]:x \in X, s \in S\}$. Essentially, its the theory $X$ whose axiom schemas take their formulas from $S$.

For example $ZF[\text{formulas in the language of set theory}]$ is just ZF, and $ZF[\text{formulas in the language of set theory + epsilon calculus}]$ is the theory I described above that was stronger than ZFC.

Now finally, the question!

For all theories $X$ and languages $L$ (which include predicate logic), does $Con(X[L]) \implies Con(X[L+\text{epsilon calculus}])$.

Answer 1

Even if you're looking at extensions of ZFC, the answer is still yes. Consider the theory of ZFC plus the scheme asserting that there is no definable global choice function. That is, the formulas "the class defined by $\varphi(x,y) $ is not a global choice function."

This theory is equiconsistent with ZFC, since if we force to add a Cohen real, then there is no (parameter-free) definable choice function, since $V\neq\text{HOD}$ in the extension.

But if we add the $\varepsilon$ operator, as you pointed out, there would now be a definable choice function in the new language, and so the scheme asserting there isn't one becomes inconsistent.