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?

11more comments