The Soundness Theorem for first-order logic

1. Introduction

The Soundness Theorem is the theorem that says that if $Σ ⊢ σ$ in first-order logic, then $Σ ⊨ σ$ , i.e. every structure making all sentences in $Σ$ true also makes $σ$ true.

The main idea is sketched out in The Mathematics of Logic, but the formal proof needs the precise definition of truth which was omitted from the printed book for technical reasons. This web page provides the missing proof and should be read in conjunction with the printed book (especially Section 9.1 and Definition 9.8 on page 122 where the proof system for first-order logic is given) and the companion web page containing the definition of truth.

Like the definition of truth itself, the main problem is how to handle free-variables. Since variables are variable they have a meaning that is apparently allowed to change, and Soundness is all about meaning. The proof of Soundness is, like all soundness theorems, by induction on the length of a proof, and $Σ$ itself may be a set of sentences but to handle all subproofs we need an induction assumption that covers all possible statements that can be present as the assumptoin of a subproof, and these include arbitrary formulas with free variables. Therefore our induction hypothesis must say what to do with free variables.

The theorem we shall actually prove is the following strengthening of the Soundness Theorem. This has Soundness as an immediate corollary, and is also stated in such a way as to indicate the correct induction hypothesis for our proof.

Theorem.

Suppose $L$ is first-order language with set of variables ${VAR}_{L}$ and $M$ is any structure for $L$ . Then:

whenever $Σ$ is a set of formulas of $L$ , $p$ is a formal proof of $σ$ from the given statements $Σ$ , and $a : {VAR}_{L} \to M$ is an assignment such that $a (τ) = ⊤$ for all $τ \in Σ$ , then $a (σ) = ⊤$ .

Proof.

By induction on the length of the proof $p$ . We shall assume that the itemised statement is true for all proofs $p$ with at most $n$ steps and show it true for a proof of $n + 1$ steps. It is important that the statement we are doing induction on ranges over all possible sets $Σ$ , and assignments $a$ , for as we shall see these vary during he course of this argument.

For the case of a proof of only one step there is nothing to say, since any proof with only a single step is either one using the given statements rule and this means the conclusion $σ$ is the same as one of the assumptions $τ \in Σ$ , so $a (σ) = a (τ) = ⊤$ , or else it is a proof of the trivially true statement $⊤$ , or of the statement $(t = t)$ by the Reflexivity rule. This last statement has $a ((t = t)) = ⊤$ since $=$ is itself reflexive and $a ((t = s)) = ⊤$ if and only if $a (t) = a (s)$ .

The rest of this argument follows the list of allowed proof steps given in Definition 9.8. See also the more detailled list of proof steps in web pages on proofs as trees and on substitution in first order logic.

Subproof.

Propositional logic rules

If the last step in the proof being considered is one of the rules of propositional logic, then we mimic the proof of the Soundness Theorem for propositional logic, given in Theorem 7.10, page 84, using the specific boolean algebra $2 = \{⊤\}, ⊥$ . This is left as an exercise.

Subproof.

Equality rules

If the last step in the proof being considered is one of the equality rules, there are three cases corresponding to reflexivity, symmetry and transitivity. These are all straightforward, following from the reflexivity, symmetry and transitivity of $=$ and the clause in the definition of truth saying that $a ((t = s)) = ⊤$ if and only if $a (t) = a (s)$ .

Subproof.

Substitution rule

If the last step in the proof being considered is the substitution rule, then we use the results of a previous web page on semantic aspects of substitution. In particular, we may assume that some $T (θ) = θ (t_{1}, t_{2}, \dots, t_{k})$ is proved from $Σ$ in at most $n$ steps and also that $(t_{i} = s_{i})$ for $i = 1, \dots, k$ are also all proved from $Σ$ in at most $n$ steps, and that the conclusion $σ$ is $S (θ) = θ (s_{1}, s_{2}, \dots, s_{k})$ where $T, S$ are the substitutions $T : v_{i} \mapsto t_{i}$ and $S : v_{i} \mapsto s_{i}$ . Then $a ((t_{i} = s_{i})) = ⊤$ by our induction hypothesis and so $a (t_{i}) = a (s_{i})$ for each $i$ , hence $a (S (θ)) = a (T (θ)) = ⊤$ by a a previous proposition on substitution and the induction hypothesis once more.

Subproof.

∃-Elimination rule

If the last step in the proof being considered is the ∃-Elimination rule, then we are given that $Σ ⊢ v ϕ$ in at most $n$ proof steps, and $Σ, S (ϕ) ⊢ σ$ in at most $n$ proof steps, where the substitution $S$ is $v \mapsto u$ , also that the substitution $S (ϕ)$ is valid and $u$ does not appear free in $σ$ nor $ϕ$ nor in any other formula written down in scope. Then ∃-Elimination gives us the conclusion $σ$ in at most $n + 1$ steps: we must show this conclusion is sound.

Let $a$ be an assignment such that $a (ψ) = ⊤$ for each $ψ \in Σ$ . Then by induction $a (v ϕ) = ⊤$ also. This means that there is some value $x \in M$ such that the assignment $b = a [x / v]$ has $b (ϕ) = ⊤$ . Let $S$ be the substitution $v \mapsto u$ and $c = a [x / u]$ . Then $c (u) = b (v)$ so $c (S (ϕ)) = b (ϕ) = ⊤$ . Also, for each $ψ \in Σ$ , $c (ψ) = a (ψ) = ⊤$ since $u$ is not free in $ψ$ , and therefore by induction and $Σ, S (ϕ) ⊢ σ$ we have $c (σ) = ⊤$ . It follows that $a (σ) = ⊤$ since once again $a, c$ only differ at $u$ which is not free in $σ$ , and this is the required conclusion.

Subproof.

∃-Introduction rule

If the last step in the proof being considered is the ∃-Introduction rule, then we may assume that $Σ ⊢ S (ϕ)$ in at most $n$ steps and $σ$ is the statement $v ϕ$ , where the substitution $S$ is $v \mapsto t$ for some $t$ . Then given an assignment $a$ with $a (ψ) = ⊤$ for each $ψ \in Σ$ , we have $a (S (ϕ)) = ⊤$ by our induction hypothesis. Let $x = a (t)$ , the element of $M$ to which $t$ is assigned by $a$ . Also let $b = a [x / v]$ . Then $⊤ = a (S (ϕ)) = b (ϕ)$ . It follows from the definition of assignment that $a (v ϕ) = ⊤$ since $b = a [x / v]$ makes $ϕ$ true.

Subproof.

∀-Elimination rule

If the last step in the proof being considered is the ∀-Elimination rule, then we argue in a similar way to the case for ∃-Introduction. We have $Σ ⊢ \forall v ϕ$ in at most $n$ steps, and we are given some term $t$ . Then for any assignment $a$ with $a (ψ) = ⊤$ for each $ψ \in Σ$ we have $a (\forall v ϕ) = ⊤$ by the induction hypothesis. Now let $S$ be the substitution $v \mapsto t$ and $x = a (t)$ . Then $b = a [x / v]$ has $b (ϕ) = ⊤$ and hence $a (S (ϕ)) = ⊤$ , as required.

Subproof.

∀-Introduction rule

If the last step in the proof being considered is the ∀-Introduction rule, then we argue in a similar way to the case for ∃-Elimination. We are given $ϕ$ and variables $u, v$ and substitution $S : v \mapsto u$ and have that $Σ ⊢ S (ϕ)$ in at most $n$ steps, where no statement written down that is in scope has $u$ free. Let $a$ be an assignment with $a (ψ) = ⊤$ for all $ψ \in Σ$ and let $x \in M$ be arbitrary. Let $b = a [x / v]$ . Then let $c = a [x / u]$ and observe that $c (ψ) = ⊤$ for all $ψ \in Σ$ since $u$ does not appear free in any such $ψ$ and hence by induction $c (S (ϕ)) = ⊤$ . But $b (ϕ) = c (S (ϕ))$ and therefore the concusion is that $b (ϕ) = ⊤$ and hence $a (\forall v ϕ) = ⊤$ as $x$ was arbitrary.

2. Exercises

Definition.

A boolean valued model for the first order language $L$ is a set $M$ with a boolean algrebra $B$ and special elements $c \in M$ for each constant symbol $c$ of $L$ , functions $F : M^{k} \to M$ for each $k$ -ary function symbol $F$ of $L$ and for $=$ and for each $k$ -ary relation symbol $R$ of $L$ it has a function $V_{=} : M \times M \to B$ and $V_{R} : M^{k} \to B$ so that $V_{=} (a, b)$ says how true $a = b$ is, and $V_{R} (a_{1}, \dots, a_{k})$ says how true $R (a_{1}, \dots, a_{k})$ is.

Exercise.

State and prove a Soundness Theorem for boolean valued models.