Skip to main content
1 of 2
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k

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.

Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k