Is there a definition of the existential quantifier which does not imply the axiom of choice?

Question

The definition of the existential quantifer given in Bourbaki's Theory of Sets is

$$(\exists x)R \iff (\tau_x(R)\mid x)R.$$

Here $x$ is a letter, $R$ is a relation, and $(\tau_x(R)\mid x)R$ means substitute $\tau_x(R)$ for $x$ in $R$. We interpret $x$ as a set, $R$ as expressing a property of $x$, and $\tau_x(R)$ as a distinguished object with the property $R$. Hence "there exists $x$ such that $R$" is equivalent to "$\tau_x(R)$ satisfies $R$".

In particular, if $A$ is a set, $(\exists x)(x \in A)$ is equivalent to $\tau_x(x \in A) \in A$. If $f$ is a surjection of $A$ onto a set $B$, then for all $y \in B$ there exists $x \in A$ such that $y = f(x)$. Therefore, we can define a right inverse $g$ of $f$ by $$g(y) = \tau_x(x \in A \text{ and } y = f(x))$$ for $y \in B$. This implies the axiom of choice.

Is there a definition of the existential quantifier which does not imply the axiom of choice? I am only familiar with Bourbaki's definition.

Answer 1

The symbols for quantifiers used in Nicolas Bourbaki, Elements of Mathematics : Theory of sets (1968 - French ed. 1958), see page 20 and page 36, are derived from The Epsilon Calculus developed by David Hilbert during the 20s [with $\tau_x$ in place of $εx$].

The syntax of the $ε$ symbol is:

if $A$ is a formula and $x$ is a variable, $εx \ A$ is a term

with the axiom (Hilbert's “transfinite axiom”) :

$A(x) → A(εx A)$.

The intended interpretation is that $εx \ A$ denotes some $x$ satisfying $A$, if there is one.

Quantifiers can defined as follows:

$∃x A(x) ≡ A(εx A)$

$∀x A(x) ≡ A(εx (¬A)).$

---

Of course, in classical logic, the usual quantifiers are interdefineable.