How does the Soundness Theorem follow from this lemma?

Question

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?

Answer 1

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 :

• Dirk van Dalen, Logic and Structure (5th ed - 2013), page 67 :

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

Answer 2

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