2
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ I think that "invertible" is not right. It seems to me that you want to check if the rule is sound, i.e.assuming that the upper seq is valid, then also the lower one is. $\endgroup$ – Mauro ALLEGRANZA May 14 '14 at 6:36
  • $\begingroup$ @MauroALLEGRANZA I thought soundness would be checked by showing that if the bottom rule holds, then the upper rule holds? $\endgroup$ – Guildenstern May 14 '14 at 6:49
  • $\begingroup$ But your argument is : "Assume that $A[x'/x]$ does not hold," which is not "Assume that $\exists x A$ does hold,"... $\endgroup$ – Mauro ALLEGRANZA May 14 '14 at 6:59
  • $\begingroup$ @MauroALLEGRANZA Well you're right that I want to show that if the upper rule is valid, then the bottom one is. I guess I got invertibility and soundness mixed up. I guess invertibility would be shown by proving that if the bottom rule is valid, then the upper one is? $\endgroup$ – Guildenstern May 14 '14 at 7:03
  • $\begingroup$ Yes; also if in the book I've cited in my answer, invertibility has a "technical" meaning which is a little bit different. I suggest you to check on your textbook... $\endgroup$ – Mauro ALLEGRANZA May 14 '14 at 7:07
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I assumed that the left sequent was valid by making the antecedent ($Gamma \dots$) not hold in it, which to my mind would did not necessarily imply that the antecedent in the right sequent would be false. Maybe I should have made that more clear. $\endgroup$ – Guildenstern May 14 '14 at 6:54
  • $\begingroup$ "But we have no "conditions" on the fresh variable $x′$ [...] Thus, $A_{x'}^x$ will be false for every possible "value" we can pick" - I don't understand this part. What if we just picked an unlucky $x'$? Isn't $x'$ an actively picked variable, a variable that might fail to help us? What if some interpretation of, say $A_{x''}^x$ was in our structure, but $A_{x'}^x$ was not? There must be some thing about this replacement of variables that I don't understand. $\endgroup$ – Guildenstern May 14 '14 at 15:09
  • $\begingroup$ @Guildenstern - I think that we have to go in deep into the definition of truth for a formula $A(x)$ with a free variable: what is the def you have in your textbook ? The soundeness of the rule is due to the fact that $\vdash (\exists x\alpha \rightarrow \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, if $x$ does not occur free in $\beta$. Thus, from $\Gamma \vdash (\alpha \rightarrow \beta)$, if $x \notin FV(\Gamma)$, by Gen Th, we derive : $\Gamma \vdash \forall x(\alpha \rightarrow \beta)$ and so, by the fact above : ... 1/2 $\endgroup$ – Mauro ALLEGRANZA May 14 '14 at 15:58
  • $\begingroup$ ... we conclude : $\Gamma \vdash (∃xα→β)$, provided that $x$ is not free in $\Gamma$ nor in $\beta$. In seq calculus, the "formalism" is a little bit different, but the "logical laws" must be the same. 2/2 $\endgroup$ – Mauro ALLEGRANZA May 14 '14 at 16:00
  • $\begingroup$ The "tricky" point is : what does it means that $\vDash A[x'/x] \rightarrow D$ when $A[x'/x]$ has a free variable ? The "standard" semantics for $P(x)$ is : $\mathcal M \vDash P(x)$ iff $P[\overline a/x]$ is true for every $a \in |\mathcal M|$. $\endgroup$ – Mauro ALLEGRANZA May 14 '14 at 16:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.