Having trouble understanding the derivation of the universal quantifier in the epsilon calculus

Question

These equations describe the derivation of the existential and universal quantifiers in the epsilon calculus: $$ \begin{align} \exists xA(x)&\equiv A(\epsilon xA)\\ \forall xA(x)&\equiv A(\epsilon x(\neg A)) \end{align} $$ The first makes intuitive sense to me: if I understand it correctly, it says that "there exists an x such that A(x) is true" is equivalent to "A is true for some x that satisfies A".

The second equation, however, makes less sense to me. It seems to be saying "for all x, A(x) is true" is equivalent to "A is true for some x that satisfies not-A". Yet the latter sounds like a contradiction.

I suspect my problem is that I don't fully understand how the epsilon operator behaves when there is no value that satisfies the predicate. Wikipedia says that "it returns some default or arbitrary term" when this is the case. Is that what's happening in the second equation? Is it just saying "when A is true for all x, the epsilon operator will fail to pick out a value satisfying not-A, so it'll just represent a value that satisfies A"?

I guess it just seems strange to me to have an operator that "tries" to pick out a value that satisfies a predicate but has a "fallback" that doesn't satisfy the predicate. Am I conceptualizing this wrong?

Answer 1

I don't think you're conceptualizing it wrong. The operator $\epsilon x(A)$ is defined to return an object satisfying $A$ if one exists, or else to return any old object. If this seems weird and non-constructive, that's because it is. But it's perfectly well defined from a classical math perspective where we have existence without explicit witnesses and the axiom of choice.

Here is the full argument for equivalence:

If $\forall x A(x)$ holds, then $\epsilon x(\lnot A)$ will be some arbitary term $t$ and since $\forall x A(x),$ holds, certainly $A(t) = A(\epsilon x(\lnot A))$ holds. Conversely, if there is an $x$ such that $\lnot A(x)$ holds, then $t=\epsilon x(\lnot A)$ will be an object such that $\lnot A(t)$ holds, so $A(\epsilon x(\lnot A))$ will be false.

Answer 2

Is it just saying "when A is true for all x, the epsilon operator will fail to pick out a value satisfying not-A, so it'll just represent a value that satisfies A"?

Indeed.

Or in other words, in a model where $\forall x\,A(x)$ holds, the rules of the logic tells us nothing about the value of the term $\epsilon x(\neg A(x))$.

All we know is that when we evaluate it, we'll consistently get something. However, this is enough to know that this value is something that $A$ is true for -- because we have explicitly assumed that $A$ is true about everything. So it doesn't matter which element of the model $\epsilon x(\neg A(x))$ gives us then.

If we do semantics (model theory) for the $\epsilon$-calculus, we need to assume that the model must know which element it picks for every possible $\epsilon$-term (and with every possible set of parameters, if the term has free variables). This makes models in that setting rather complex beasts -- at least compared to standard first-order logic.

For example, a model for arithmetic would give some definite number that is $\epsilon x(2 \mid x)$ (that is, "the canonical even number"), and the claim $3\mid \epsilon x(2\mid x)$ would have some definite truth value which is not forced by saying that our model consists of the usual integers. Similarly $\epsilon x(x=x+1)$ (a property that no number has!) would have some definite value, and we'd be able to ask whether it happens to be $42$ or not. Perhaps it is, perhaps not.