2
$\begingroup$

The soundness theorem is a famous theorem in logic that goes like this:

If $\Gamma \vdash \phi$, then $\Gamma \vDash \phi$.

It's supposed to follow readily from Lemma 3.2.3 from Moerdijk/Van Oosten's Sets, Models and Proofs:

Lemma 3.2.3 Suppose $T$ is an $L$-labelled proof tree with unmarked assumptions $\phi_1,\ldots,\phi_n$ and conclusion $\psi$; let $u_1,\ldots,u_k$ be a list of all varialbes that are free in at least one of $\phi_1,\ldots,\phi_n,\psi$. Then for every $L$-structure $M$ and any $k$-tuple $m_1,\ldots,m_k$ of elements of $M$, we have:

If for all $i, 1\le i\le n, M \models\phi_i[m_1/u_1,\ldots,m_k/u_k]$, then $M \models\psi[m_1/u_1,\ldots,m_k/u_k]$.

Can anyone explain to me why that is?

$\endgroup$
  • 1
    $\begingroup$ What book (title, author, etc.) is the lemma from? $\endgroup$ – user642796 Aug 29 '15 at 15:28
  • $\begingroup$ staff.science.uu.nl/~ooste110/syllabi/setsproofs09.pdf $\endgroup$ – Riley Aug 29 '15 at 15:31
  • $\begingroup$ Are you clear about the definitions of the two "turnstile" symbols and the meaning of the claim in your "soundness theorem"? $\endgroup$ – hardmath Aug 29 '15 at 15:34
  • $\begingroup$ Hint: to solve Exercise 91 in those nice notes, observe that it comes just after a section entitled "Induction on Proof Trees". $\endgroup$ – Rob Arthan Aug 29 '15 at 15:41
  • $\begingroup$ @hardmath, yes I'm studying those concepts right now. And I'll try induction, see where it takes me :) $\endgroup$ – Riley Aug 29 '15 at 15:43
4
$\begingroup$

The soundness property of a logical calculus means that if a formula $\phi$ is derivable form the set $\Gamma$ of premises (or assumptions) :

$\Gamma \vdash \phi$,

then $\phi$ is a logical consequence of the premises in $\Gamma$, according to the semantics suitable for that calculus :

$\Gamma \vDash \phi$.


The application of the said Lemma is roughly this; let $\Gamma = \{ \varphi_1, \ldots, \varphi_n \}$ the set of assumptions and let $\psi$ the conclusion of the derivation (the proof tree) [see page 81 of your lecture notes].

We assume that, for any structure $M$ "suitable" for the language $L$ [see page 42 of your lecture notes], the premises are all true (or satisfied) in $M$ : $M \vDash \varphi_i$ [see page 43].

The rules of the calculus are defined exactly in a way to be sound, i.e. such that if the premises of the rules are true (in a strucutre $M$) so is the conclusion [this is the gist of the proof of the Lemma, page 88, where some rules are treated in detail].

Thus, any step in the derivation "transfer" truth from the previous one and thus, if all the premises in $\Gamma$ are true in $M$, so is the conclusion $\psi$ : $M \vDash \psi$.

But this is exactly the definition of logical consequence : $\Gamma \vDash \psi$ [see page 50].


See e.g :

We say that $\varphi$ is a semantic consequence of $\Gamma$ if $\Gamma \vDash \varphi$, i.e. $\varphi$ holds in each model of $\Gamma$ [where : $\Gamma \vDash \varphi$ ϕ iff (if $M \vDash \Gamma$, then $M \vDash \varphi$)].

$\endgroup$
  • 2
    $\begingroup$ Wow! I know you're not supposed to say "thank you" in the comments, but this answer is just too good, so I have to say it: Thank you, Mauro! $\endgroup$ – Riley Aug 29 '15 at 16:17
1
$\begingroup$

Mauro's answer is very helpful and clear. I'd just like to add to it one point.

Granted the context of the lemma you mention, that lemma isn't just a restatement of soundness but a slight generalization.

Recall that, roughly speaking, soundness says that derivability implies consequence. However, this rough statement is not strictly true for some systems which are intuitively sound. The reason is that derivability may relate formulas with free variables, whereas consequence, as its construed in the notes, applies only to formulas which are true-or-false in a structure, which is to say closed formulas.

As Mauro says, "$\psi$ is a consequence of $\Gamma$" means there's no $M$ such that $M\models \Gamma$ but $M\not\models \psi$. So, and I think this is how it's construed in the cited notes, consequence is a relation on formulas which are true-or-false in an arbitrary structure for the language. For example, $Fx$ will not even be a consequence of $Fx$. Rather, if a formula $\phi$ contains free variables $u_1,\ldots,u_k$, then it is true in $M$ only relative to a substitution $m_1/u_1\ldots,m_k/u_k$ of constants-from-$M$ for those variables.

On the other hand, derivability is a relation on arbitrary formulas. For example, $Fx$ is certainly derivable from $Fx$. Thus, $Fx$ is derivable from itself but not a consequence of itself, and the rough statement of soundness fails.

Happily, consequence can be generalized a notion of free-variable consequence, which applies to open formulas.

$\psi$ is a free-variable consequence of $\phi_1,\ldots,\phi_k$ iff for every $M$ and every $M$-substitution $m_1/u_1,\ldots,m_k/u_k$ for $u_1,\ldots,u_k$ we have that $M\models\psi[m_1/u_1,\ldots,m_k/u_k]$ whenever $M\models \phi_i[m_1/u_1,\ldots,m_k/u_k]$ for all $i$.

Now, the lemma you mention says: "derivability implies free-variable consequence". When "derivability implies consequence" is restricted to closed formulas, it follows immediately from the lemma.

(The need to pass through a special free-variable notion of consequence turns a bit on then notes' choice of a Shoenfield-style rather than Tarskian semantics for the quantifiers.)

$\endgroup$
  • $\begingroup$ It seems to me that $F(x) \vdash F(x)$ and also $F(x) \vDash F(x)$, so the example mentioned is not clear to me. Perhaps you have a different convention about what it means for a model to satisfy a formula with free variables? But, whatever $M \vDash F(x)$ means, it seems to me that if $M \vDash F(x)$ then $M \vDash F(x)$, so $F(x)$ should be a consequence of itself. $\endgroup$ – Carl Mummert Aug 29 '15 at 16:38
  • $\begingroup$ Many authors include a variable substitution as part of a model $M$, so that for every formula $\phi$ we have $M \vDash \phi$ or $M \vDash \lnot \phi$. Perhaps the example was coming from the other perspective where $\vDash$ is only defined for sentences? $\endgroup$ – Carl Mummert Aug 29 '15 at 16:42
  • $\begingroup$ Yes, on a Tarski-style understanding of consequence, then $Fx$ is a consequence of itself, so soundness and derivability coincide. But I was hoping to follow the convention of the notes. So construed, a model doesn't satisfy a formula with free variables absolutely, but only relative to a replacement of those variables with parameters. In contrast, the consequence as explained on page 50 doesn't relativize truth to a notion of replacement. $\endgroup$ – mmw Aug 29 '15 at 16:44
  • $\begingroup$ At least according to the definitions of structure and of truth on pages 42-43, it looks like a variable-substitution isn't built into a structure. $\endgroup$ – mmw Aug 29 '15 at 16:47

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.