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?

  • $\begingroup$ Also mathoverflow.net/questions/281301/… $\endgroup$
    – Asaf Karagila
    Mar 8, 2018 at 22:51
  • $\begingroup$ Also, in the second inference rule you have $p(x)$ and $q(x)$, and then $p(x)$ and $p(y)$. Something is off... $\endgroup$
    – Asaf Karagila
    Mar 9, 2018 at 0:14
  • 2
    $\begingroup$ 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? $\endgroup$ Mar 9, 2018 at 0:33
  • 1
    $\begingroup$ @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. $\endgroup$ Mar 9, 2018 at 2:36
  • 2
    $\begingroup$ 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. $\endgroup$ Mar 9, 2018 at 8:35


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.