Soundness of existential quantifier ($\exists \vdash$) in Gentzen's system

Question

Consider Gentzen's system for first order logic with sequents $\Gamma \vdash_G \Delta$, where $\Gamma$ and $\Delta$ are finite sets of formulae.

One of the rules in Gentzen is:

$$(\exists\vdash) \, \, {\Gamma, A_{x'}^x \vdash_G \Delta \over \Gamma, \exists xA \vdash_G \Delta}\ x' \, \text{fresh} $$

Theorems are proved by using these kind of rules "bottom up"; you start with the theorem you want to prove on the lowest line, and then use the rules to build yourself upwards, until you hopefully terminate with a axiom(s) on the last line(s).

A sequent $A_1, A_2, \dots, A_n \vdash_G B_1, B_2, \dots, B_m$ is equivalent to $A_1 \wedge A_2 \wedge \dots \wedge A_n → B_1 \vee B_2 \vee \dots \vee B_m$. This means that a satisfied sequent can be expressed as $M \models \bigwedge \Gamma → \bigvee \Delta$, where $M$ is a structure.

Question: In light of the above, I can't see how the rule ($\exists \vdash$) is sound. Namely, I can't see how:

$M \models \bigwedge \Gamma \wedge A_{x'}^x → \bigvee \Delta \implies M \models \bigwedge \Gamma \wedge \exists xA → \bigvee \Delta$

Assume that $A_{x'}^x$ does not hold, which means that $M \not\models \bigwedge \Gamma \wedge A_{x'}^x$. This should force $\bigwedge \Gamma \wedge \exists xA$ to not hold, but it is my impression that it may hold; consider if there really does exist an $x$ such that $A$, only it was not that particular $x'$ ($A_{x'}^x$). We are allowed to be "unlucky", ie. choose a fresh variable that may not yield a formula that is in the structure. But $\exists xA$ should still hold, I think, if there really is some $x$ that we may not have found yet s.t. $A$ holds. But since we are not guaranteed (it seems) that the antecedent in the sequent on the right side is false when the antecedent in the sequent on the left side is false, the given formula (the one experessing that it should be sound) can not hold; if the antecedent in the left sequent does not hold, then the antecedent of the right sequent may still hold. This in turn means that the whole formula does not hold if the consequent does not hold (which is the same in both sequents).

Answer 1

The rule is sound, i.e. if the upper sequent is valid, then also the lower one is.

This does not license us to conclude anything from the fact that the upper sequent is false.

This situation is common to all inference rules of any logical calculus : think at modus ponens.

In sequent calculus, there is a property caleld invertibility [see Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 71] which - in this case - says that :

if $\vdash \exists x A, \Gamma \implies D$, then $\vdash A[y/x], \Gamma \implies D$.

It is expressed in term of derivability, but of course can be "read" also in term of validity; but, again, it says that if the left sequent is valid, so is the right one.

Added

Consider the rule :

$$(\exists\vdash) \, \, {\Gamma, A_{x'}^x \vdash_G D \over \Gamma, \exists xA \vdash_G D}\ x' \, \text{fresh} $$

and forget about the "context" $\Gamma$.

The rule may be read as a meta-rule relative to the derivability relation : $\vdash$.

We may read it as :

if $A_{x'}^x \vdash_G D$ , then $\exists xA \vdash_G D$, provided that $x \notin FV(D)$.

We want that the rules of the calculus are sound, i.e. that:

if $A_{x'}^x \vDash D$ , then $\exists xA \vDash D$

which can be equivalently translated (as you say) into :

if $\vDash A_{x'}^x \rightarrow D$ , then $\vDash \exists xA \rightarrow D$.

Now we will check if the rule is sound.

Case 1 : if $D$ is true, then both the upper sequent and the lower sequent are true.

Case 2 : $D$ is false, and assume that $\exists xA$ is true. This means that there is in the domain of the interpretation a possible "value" for the variable $x$ such that $A(x)$ is true.

If we "pick" this object ad use it as "value" for the variable $x'$, we have that for this object also $A_{x'}^x \rightarrow D$ is false, contrary to the assumption that it is valid.

Thus, in this case, is not possible that $\exists xA$ is true and we have that the lower sequent is true.

Conclusion : the lower sequent it valid

---

Note

If the "informal" argument for soundness is not "strong" enough, I will try with a more formal one.

I'll adopt the semantic of Herbert Enderton, A Mathematical Introduction to Logic, (2nd - 2001), SECT 2.2 : Truth and Models [page 80-on] :

we will define what it means for $\mathcal M$ to satisfy $\varphi$ with $s : Var \rightarrow |\mathcal M|$; in symbols : $\mathcal M \vDash \varphi[s]$.

Then we have the condition for the quantifiers :

$\mathcal M \vDash \exists x \varphi[s]$ iff for some $d \in |\mathcal M|$, we have $\mathcal M \vDash \varphi[s(x/d)]$, where $s(x/d)$ is the function which is exactly like $s$ except for one thing: at the variable $x$ it assumes the value $d$.

Finally, we have that [page 88] :

$\varphi$ is valid iff for every $\mathcal M$ and every $s : Var \rightarrow |\mathcal M|$, $\mathcal M$ satisfies $\varphi$ with $s$.

Now we must apply it to :

$\vDash A_{x'}^x \rightarrow D$, with $x \notin FV(D)$.

But $A_{x'}^x$ is $A(x')$ with $x'$ free; thus we have $\mathcal M \vDash (A(x') \rightarrow D)[s]$, for every $\mathcal M$ and every $s$.

Fix $\mathcal M$; to say "every $s$" is equivalent to say "$s(x'/d)$, for every $d \in |\mathcal M|$". Thus, $\mathcal M \vDash A_{x'}^x \rightarrow D$ iff $\mathcal M \vDash (A(x') \rightarrow D)[s(x'/d)]$, for every $d \in |\mathcal M|$.

But this amount to : $\mathcal M \vDash \forall x (A(x) \rightarrow D)[s]$.

But $x$ is not free in $D$; thus :

$\mathcal M \vDash (\forall xA(x) \rightarrow D)[s]$.

This holds for every $\mathcal M$ and every $s$; thus we may conclude :

$\vDash \forall xA(x) \rightarrow D$.

Now, we go back to the above "informal" argument and spell it with the formal semantic specifications.

Suppose that $A_{x'}^x \rightarrow D$ is valid and that $x$ is not free in $D$, and suppose that $(\exists xA \rightarrow D)$ is false, for some $\mathcal M$.

Then $\exists xA$ is true and $D$ is false.

From the former, $A[s(x'/d)]$ is true for some $d$; so $(A_{x'}^x \rightarrow D)[s(x'/d)]$ is false in $\mathcal M$ [here we need the proviso that $x \notin FV(D)$].

This is impossible, since $(A_{x'}^x \rightarrow D)$ is valid, i.e. for every $\mathcal M$ and every $s$ : $\mathcal M \vDash (A_{x'}^x \rightarrow D)[s]$.

Thus, $(\exists xA \rightarrow D)$ is true for $\mathcal M$. But $\mathcal M$ is an interpretation whatever; thus the formula is valid.