0
$\begingroup$

I'm currently reading a pdf textbook called Sets, Logic, Computation An Open Introduction to Metalogic Remixed by Richard Zach, and it covers sequent calculus LK and (partially) proves its soundness. I've been trying to prove soundness for myself but I've run into a few issues. I'm trying to prove soundness in the standard way, i.e., by induction on the inference rules, i.e., by showing each inference rule preserves validity.

I'm using the book's definition of a sequent satisfaction and validity:

Definition 8.27. A structure $M$ satisfies a sequent $\Gamma\Rightarrow\Delta$ iff either $M\not\models A$ for some $A\in\Gamma$ or $M\models A$ for some $A\in\Delta$. A sequent is valid iff every structure $M$ satisfies it.

(page 155)

I'm confused about the interpretation of a sequent. At the beginning the of chapter it states:

The intuitive idea behind a sequent is: if all of the sentences in the antecedent hold, then at least one of the sentences in the succedent holds. That is, if $\Gamma=\langle A_1,\ldots,A_m\rangle$ and $\Delta=\langle B_1,\dots,B_n\rangle$, then $\Gamma\Rightarrow\Delta$ holds iff $$(A_1\land\dots\land A_m)\rightarrow(B_1\lor\dots\lor B_n)$$ holds.

(page 135)

But this interpretation is slightly different from sequent satisfication and validity. In the former case (sequent intuition), the variable assignment function is shared across all wffs in $\Gamma=\langle A_1,\ldots,A_m\rangle$ and $\Delta=\langle B_1,\dots,B_n\rangle$, i.e., $$M,s\models((A_1\land\dots\land A_m)\rightarrow(B_1\lor\dots\lor B_n))\quad\text{(Soundness$_1$)}$$ for every structure $M$ and every variable assignment function $s$ of $M$. In the latter case (sequent satisfaction/validity), each wff in $\Gamma=\langle A_1,\ldots,A_m\rangle$ and $\Delta=\langle B_1,\dots,B_n\rangle$ has its own bounded variable assignment function, i.e., $$(M\models A_1\land\dots\land M\models A_m)\rightarrow(M\models B_1\lor\dots\lor M\models B_n)\quad\text{(Soundness$_2$)}$$ for every structure $M$. Both of these interpretations say something logically different, yet they're treated as equivalent.

For example, when the book talks about eigenvariable conditions, it justifies them by appealing to validity preservation (Soundness$_2$):

In $\exists R$ and $\forall L$ there are no restrictions on the term t. On the other hand, in the $\exists L$ and $\forall R$ rules, the eigenvariable condition requires that the constant symbol a does not occur anywhere outside of $A(a)$ in the upper sequent. It is necessary to ensure that the system is sound, i.e., only derives sequents that are valid.

(page 138)

But other interpretations justify them by appealing to Soundness$_1$:

Concerning the rule $\exists$-$L$, first you have to recall that this rule (as well as the rule $\forall$-$R$) is valid only if the variable $y$ does not occur free within $\Gamma$ and $\Delta$. The intuitive meaning of the rule is the following. Suppose that under the hypotheses $\Gamma$ and $\phi[y]$ you can derive $\Delta$ (this is the premise of the rule $\exists$-$L$). Now, since $y$ does not occur free in $\Gamma$ and $\Delta$, this means that you didn't make any hypothesis about $y$, so the fact that $\Delta$ derives from $\Gamma$ and $\phi[y]$ actually means that you can derive $\Delta$ from $\Gamma$ and $\phi[y]$, for any value of the variable $y$. In other words, to derive $\Delta$ it is enough to suppose $\Gamma$ and the fact that there exists an $x$ such that $\phi[x/y]$, that is, under the hypotheses $\Gamma$ and $\exists x\phi[y/x]$ you can derive $\Delta$ (this is the conclusion of the rule $\exists$-$L$).

(link)

On further inspection, I found this sequent derivation, $$\frac{x<y\Rightarrow x<y}{\Rightarrow x<y,\lnot x<y}\lnot R$$ where $x$ and $y$ are variables and $<$ is a binary relation of the language. Notice that under the arithmetic interpretation, where the universe of discourse is $\mathbb{N}$ and $<$ is interpreted as the standard 'less than' relation, the sequent $\Rightarrow x<y,\lnot x<y$ is not valid in terms of Soundness$_2$ since $M,s\not\models x<y$ when $s(x)=2$ and $s(y)=1$ and since $M,s\not\models\lnot x<y$ when $s(x)=1$ and $s(y)=2$. Therefore, sequent calculus is not sound with respect to Soundness$_2$. So it seems that the textbook definition is wrong. I do believe however (although I haven't yet proved it) that sequent calculus is sound in terms of Soundness$_1$.

I thought that maybe this was simply a textbook error and that they meant to define soundness as in Soundness$_1$. But looking at other textbooks, articles, stack exchange posts, and Wikipedia, they all seem to agree with the definition in my textbook, and it seems unlikely that all of these sources could commit the same simple error. So perhaps I'm wrong, but don't see how that is.

This is why I'm confused about soundness of sequent calculus and the interpretation of sequents. Soundness$_2$ seems to be wrong but appears to be the popular interpretation, and the Soudness$_1$ seems like the correct interpretation but doesn't appear in any source I can find. I'm not sure where to go from here.

$\endgroup$
1

1 Answer 1

2
$\begingroup$

You are right : Def.8.27 is a little bit sloppy. If the formulas involved are not sentences (i.e. they may have free variables) the definition of satisfaction must include a variable assignment function.

See G.Takeuti, Proof Theory (2nd ed. 1987), page 41 :

" A sequent $\Gamma \to \Delta$ is satisfied in $(D, \phi)$ by $\phi_0$..." where $(D, \phi)$ is a structure and $\phi_0$ is a mapping from variables to $D$.

__

Regarding validity and soundness :

valid is : satisfied by every structure and every assignment.

Soundness means either "a formula that is valid is provable, i.e. if $\vdash \varphi$, then $\vDash \varphi$" or "if $\Gamma \vdash \varphi$, then $\Gamma \vDash \varphi$".

In the second case we have :

$\Gamma \vDash \varphi$ iff for every structure $M$ and variable assignment $s$ such that $M$ satisfies every member of $\Gamma$ with $s$, $M$ also satisfies $\varphi$ with $s$."

But see Zach, page 155 :

Theorem 8.28 (Soundness). If $\mathsf {LK}$ derives $Θ ⇒ Ξ$, then $Θ ⇒ Ξ$ is valid.

And see page 158, where the rules for quantifiers are treated : "Consider a structure $M$. Since the premise $A(t), Γ ⇒ Δ$ is valid,..." that means that the sequent is satisfied in $M$ by every variable assignment $s$.

$\endgroup$
1
  • $\begingroup$ So when I prove soundness for sequent calculus, I should be proving Soundness$_1$ like I stated above? $\endgroup$
    – Kainoa B
    Commented Oct 25, 2019 at 6:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .