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}])$.

  • 3
    $\begingroup$ Why can't you just take ZF+some axiom inconsistent with choice, like determinacy ? $\endgroup$ Sep 16, 2017 at 17:38
  • $\begingroup$ @SimonHenry oh dang, dah! I should probably delete this then, giving how simple that was. $\endgroup$
    – PyRulez
    Sep 16, 2017 at 17:42
  • $\begingroup$ @SimonHenry Why go all the way to AD - just add $\neg$AC. $\endgroup$ Sep 16, 2017 at 17:59
  • 1
    $\begingroup$ @SimonHenry You should post that as an answer, to move this off the unanswered queue. $\endgroup$ Sep 16, 2017 at 21:55
  • $\begingroup$ The title question is the opposite of the question asked in the post. $\endgroup$ Sep 16, 2017 at 23:41

1 Answer 1


Even if you're looking at extensions of ZFC, the answer is still no. 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.