Is this inference correct using the existential quantifier?

Question

Suppose that one has the statement $\forall x\exists y :P(x,y)$. Given an $a$, then it follows that there is a $b$ such that $P(a,b)$.

My question is: Am I allowed to call this object $b_a$ or $b(a)$ or any other version that behaves like a function symbol? If so, why or why not?

Why am I asking this? Suppose that $X$ is a set and we have $\forall x \in X \exists y \in X: P(x,y)$ and suppose that we are allowed to introduce $b_a$ for the appropriate object as explained above. Then we know that there exists the set $A$ such that $$\forall z : z \in A \iff \exists a,b \in X : z=(a,b) \wedge =b_a$$ or in other words $$A=\{(a,b_a):a \in X\}.$$

If this were allowed, I wouldn't need the axiom of choice to construct the set $A$. However, if this wasn't allowed, I would need the axiom of choice, since I can't (or at least I don't know how to) construct such a set from the statement $\forall x \in X \exists y \in X:P(x,y)$. More precisely, I don't see how one could prove the existence of a set $A$ that consists of pairs of the elements $x$ of $X$ with exactly one element $y$ of $X$ that satisfy $P(x,y)$. If the object $y$ is unique, then this is easy: $$\forall z : z \in A \iff \exists x,y \in X: z=(x,y) \wedge P(x,y)$$ or $$A=\{(x,y) \in X \times X: P(x,y)\}$$ One possible explanation? I think in formal logic this is not allowed, but I am not sure how it is in more informal maths other than formal logic, or even why its not allowed in formal logic. One potential reason I came up with is the following. Suppose one has an object $x$ and introduces a function symbol $f(x)$ for an object $y$ that satisfies $P(x,y)$. Then, if $y_1,y_2$ are two objects that satisfy $P(x,y_1),P(x,y_2)$, one might be tempted to incorrectly infer: $P(x,y_1)$ implies $y_1=f(x)$ and $P(x,y_2)$ implies $y_2=f(x)$, thus $y_2=y_1$, where one used the intuition that function symbols should be unique objects, which they of course are not in this case. However, with enough caution, such mistakes shouldn't happen. Therefore I am not entirely sure why its not allowed to introduce those.

Answer 1

There is a precise sense in which it is acceptable to do this even without any form of the axiom of choice.

Suppose we are working in first-order logic over vocabulary $V$. And suppose we have some set of axioms $T$ and some proposition $P(x, y)$ in the variables $x, y$, and we have $T \vdash \forall x \exists y P(x, y)$. Then we can define $V' = V \cup \{f\}$, where $f$ is a unary function symbol, and define $T' = T \cup \{\forall x P(x, f(x))\}$. Then this new deductive system is a conservative extension. More formally, for any sentence $\phi$ in the language of $V$, we have $T \vdash \phi$ if, and only if, $T' \vdash \phi$.

This can be proved even without using the axiom of choice, as it is purely a syntactic fact. However, it is more convenient to prove it using the axiom of choice and the completeness theorem. For if we have any $V$-structure $M$ such that $M \models T$, then we have $M \models \forall x \exists y P(x, y)$. We then apply the axiom of choice to produce some $f^M$ such that $\forall x \in M (P^M(x, y))$. Adding $f^M$ to $M$ gives us $M'$, which is a $V'$ structure which is a model of $T'$. And of course, for any sentence $\phi$ in the language of $V$, we have $M' \models \phi$ if and only if $M \models \phi$. Thus, we see that semantically, $T'$ is a conservative extension of $T$ - for all $\phi$ in the language of $V$, we see that $T \models \phi$ iff $T' \models \phi$. Apply the completeness theorem to get the syntactic version.

In fact, we only require the ultrafilter lemma to get that $T'$ is semantically a conservative extension of $T$. So this fact does not imply the axiom of choice. However, without the axiom of choice, we cannot, in general, take a model $M$ of $T$ and extend it to a model $M'$ of $T'$, where both models are exactly the same $V$-structure. Instead, what we see is that if $M$ is a $V$-structure modelling $T$ such that $M \models \neg \phi$, then there exists some $M'$ which is a model of $T'$ and of $\neg \phi$, but there is no reason to believe that $M$ and $M'$ should be nicely related to each other by being the same $V$-structure.

In particular, if we have $\forall x \in X \exists y \in X (P(x, y))$, then we have $X \models \forall x \exists y P(x, y)$. So if we wish to make deductions in first-order logic about $X$, we could, within the first-order system, add a function symbol $a \mapsto b_a$ and the axiom $\forall x (P(x, b_x))$. But (in the absence of the axiom of choice) this would not actually mean there exists such a function $X \to X$.