3
$\begingroup$

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?

Improve this question
$\endgroup$
16
  • $\begingroup$ Also mathoverflow.net/questions/281301/… $\endgroup$
    – Asaf Karagila ♦
    Commented 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 ♦
    Commented 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$
    – Noah Schweber
    Commented 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$
    – Noah Schweber
    Commented 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$
    – Emil Jeřábek
    Commented Mar 9, 2018 at 8:35

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .