# Can we prove the epsilon theorems without the axiom of choice?

Hilbert's epsilon $\epsilon$ is a quantifier. It follows the rule that if $\exists x. p(x)$, for some predicate $p$, we can infer $p(\epsilon x. p(x))$. Semantically, it represents picking some element $x$ that satisfies $p(x)$, or an arbitrary element otherwise. Another common inference rule is that if $p(x) \equiv q(x)$, then $\epsilon x. p(x) = \epsilon y. q(y)$.

Without the axiom of choice, the semantics no longer make sense, but the syntax still does. Can we prove the epsilon theorems without it?

• Commented Mar 8, 2018 at 22:51
• Also, in the second inference rule you have $p(x)$ and $q(x)$, and then $p(x)$ and $p(y)$. Something is off... Commented Mar 9, 2018 at 0:14
• I'm a bit confused. The epsilon theorems are about derivability in a fixed formal system; these are purely combinatorial (or broadly number-theoretic) facts, and have nothing to do with the axiom of choice. (Massive overkill: the epsilon theorems are arithmetic statements, and we have absoluteness between $V$ and $L$ for such statements in ZF ...) So is this really what you're asking? Commented Mar 9, 2018 at 0:33
• @PyRulez Well, you can't have that unless your language is uncountable. But actually, since "$\vdash$" is compact, even that doesn't matter: a statement of the form "$\Gamma\vdash\varphi$" is absolute, regardless of how big $\Gamma$ is. Commented Mar 9, 2018 at 2:36
• It is reasonably clear from the linked SEP article that the original proofs were finitistic (that was kind of the whole point of the enterprise), so they wouldn’t use the axiom of choice in the first place. Commented Mar 9, 2018 at 8:35