Confusion over semantics behind ∃-elimination

Question

$\exists-$ states that: if $\Sigma, A(u) \vdash B$ where u occurs nowhere else, then $\Sigma, \exists x A(x) \vdash B$.

Why does this translate to $\exists$ and not $\forall$? Intuitively, $A(u)$ where $u$ occurs nowhere else should mean that $u$ can be any arbitrary thing, so shouldn't $\Sigma, A(u) \vdash B$ be valid for any conceivable $u$ (a.k.a, all $x$) meaning $\Sigma, \exists xA(x) \vdash B$?

This is giving me trouble mostly because of the below theorem I've already learned:

Why is it that in this case $A(u)$ can translate in to a "for all" while in $\exists-$ it only gives us "there exists"? In both cases $u$ is arbitrary, so it should refer to anything$-$"for all"$-$in my head.

Answer 1

The term $u$ is arbitrary yes, but what isn't arbitrary is the fact that we have a derivation $\Sigma, A(u) \vdash B$.

What does it mean to have $\Sigma, A(u) \vdash B$? It means that, assuming $\Sigma$ and $A(u)$ (for some particular $u$), we can prove $B$. Moreover, since $u$ doesn't appear anywhere else, it can't be a "proper" part of the proof: all that is necessary to prove $B$ is that $A(x)$ is true for some x. The $\exists- $ says precisely this, that we don't care about the specific $u$ that satisfies $A(x)$, only that there is something which satisfies it.

On the other hand, suppose we can prove $A(u)$ from $\Sigma$ without assuming $u$. This means that the proof of $A(u)$ can't really "depend" on $u$, so we should be able to prove $A(x)$ for any $x$. And this is what the $\forall +$ rule says.

Answer 2

Intuitively, $A(u)$ where $u$ occurs nowhere else should mean that $u$ can be any arbitrary thing.

No, $u$ is not arbitrary.

"Arbitrary" means: whatever term $u$ we may choose...

This is not so: we have to choose a “fresh” term, in the sense of having no other occurrences in the derivation.

We have (as per the title of your question) to consider the semantics.

With $(\forall \text I)$ rule we may, under the condition that $u$ is "fresh", derive from $A(u)$ the "generalization" $\forall x A(x)$.

Here every possible choice of a term $u$ not already used will do, and this is consistent with the intuitive meaning of the rule: if $A$ holds of an "object" $u$ whatever, then it holds of every "object".

A simple arithmetical example is: we have proved $\mathsf {PA} \vdash (x \ge 0)$, where $\mathsf {PA}$ is the collection of Peano's axioms.

Then we may apply $(\forall \text I)$ to conclude with: $\mathsf {PA} \vdash \forall x(x \ge 0)$.

Consider now the formula $\exists x (x > 0)$.

If we want to use it in a proof with $(\exists \text E)$ rule, we have to choose a suitable term $u$ for the assumption $(u > 0)$: the formula $\exists x (x > 0)$ says there must be (at least) one.

But we cannot choose an "arbitrary" term, i.e. a term whatever: for $u=0$ we get $(0 > 0)$, which is false.