# 1.5 Soundness and Completeness

Propositional logic can be studied in two complementary ways. The semantic approach studies truth under valuations, while the proof theoretic approach studies formal derivations from axioms and inference rules. Soundness and completeness explain how these two approaches are related.

### Semantic Consequence

Let $\Gamma$ be a set of formulas, and let $A$ be a formula.

We say that $A$ is a semantic consequence of $\Gamma$ if every valuation that makes all formulas in $\Gamma$ true also makes $A$ true.

We write:
$$
\Gamma \models A
$$

This means that for every valuation $v$, if:
$$
v(B)=\mathrm{T}
$$
for every $B \in \Gamma$, then:
$$
v(A)=\mathrm{T}
$$

In the special case where $\Gamma$ is empty, the notation:
$$
\models A
$$
means that $A$ is true under every valuation, so $A$ is valid.

### Example 1.34

Let:
$$
\Gamma = \{p \to q, p\}
$$

Then:
$$
\Gamma \models q
$$

Indeed, suppose $v$ is a valuation such that:
$$
v(p \to q)=\mathrm{T}
$$
and:
$$
v(p)=\mathrm{T}
$$

By the truth rule for implication, if $p$ is true and $p \to q$ is true, then $q$ must be true. Hence:
$$
v(q)=\mathrm{T}
$$

Therefore every valuation satisfying both premises also satisfies $q$.

### Formal Proof Systems

A proof system consists of formulas called axioms together with inference rules that allow new formulas to be derived from previous formulas.

A derivation from assumptions $\Gamma$ is a finite sequence of formulas:
$$
A_1, A_2, \dots, A_n
$$
where each formula $A_i$ is either an assumption from $\Gamma$, an axiom of the proof system, or follows from earlier formulas by one of the inference rules.

If there is a derivation of $A$ from $\Gamma$, we write:
$$
\Gamma \vdash A
$$

This notation means that $A$ is syntactically provable from $\Gamma$.

### Modus Ponens

The most basic inference rule for implication is modus ponens:
$$
\frac{A \qquad A \to B}{B}
$$

This rule says that if $A$ has been derived, and $A \to B$ has been derived, then $B$ may be derived.

For example, from:
$$
p
$$
and:
$$
p \to q
$$
we may infer:
$$
q
$$

This rule is purely syntactic. It operates on formulas according to their form, without directly referring to truth values.

### Definition 1.35 (Soundness)

A proof system is sound if every syntactic consequence is also a semantic consequence.

That is, for every set of formulas $\Gamma$ and every formula $A$:
$$
\Gamma \vdash A \quad \Longrightarrow \quad \Gamma \models A
$$

Soundness says that the proof system never proves a formula that fails semantically. If a formula can be derived from assumptions, then it is true under every valuation that makes those assumptions true.

### Lemma 1.36 (Soundness of Modus Ponens)

Modus ponens preserves truth under every valuation.

Proof

Suppose $v$ is a valuation such that:
$$
v(A)=\mathrm{T}
$$
and:
$$
v(A \to B)=\mathrm{T}
$$

By the truth rule for implication, the formula $A \to B$ is false exactly when $A$ is true and $B$ is false.

Since $v(A)=\mathrm{T}$ and $v(A \to B)=\mathrm{T}$, it cannot be the case that $v(B)=\mathrm{F}$.

Therefore:
$$
v(B)=\mathrm{T}
$$

Thus whenever the premises of modus ponens are true under a valuation, the conclusion is also true under that valuation.

### Lemma 1.37 (Soundness Principle)

If every axiom of a proof system is valid and every inference rule preserves truth, then the proof system is sound.

Proof

Let:
$$
A_1, A_2, \dots, A_n
$$
be a derivation of $A$ from assumptions $\Gamma$.

We prove by induction on $i$ that every valuation satisfying all formulas in $\Gamma$ also satisfies $A_i$.

If $A_i$ is an assumption, then it is true under every valuation satisfying $\Gamma$ by definition.

If $A_i$ is an axiom, then it is true under every valuation because axioms are assumed to be valid.

If $A_i$ follows from earlier formulas by an inference rule, then the earlier formulas are true under the valuation by the induction hypothesis, and the conclusion is true because the inference rule preserves truth.

Applying this to the last line $A_n=A$, we obtain:
$$
\Gamma \models A
$$

### Definition 1.38 (Completeness)

A proof system is complete if every semantic consequence is also a syntactic consequence.

That is, for every set of formulas $\Gamma$ and every formula $A$:
$$
\Gamma \models A \quad \Longrightarrow \quad \Gamma \vdash A
$$

Completeness says that the proof system is strong enough to derive every formula that is forced by the assumptions. In propositional logic, this means that truth table consequence can be captured by formal proof.

### Theorem 1.39 (Soundness and Completeness)

For a standard proof system of propositional logic:
$$
\Gamma \vdash A \quad \text{if and only if} \quad \Gamma \models A
$$

The left side is syntactic, because it refers to derivations using formal rules.

The right side is semantic, because it refers to truth under all valuations.

This theorem says that the syntactic and semantic notions of consequence coincide.

### Proof Idea

The soundness direction is proved by checking that axioms are valid and that inference rules preserve truth, as described above.

The completeness direction is more substantial. One common strategy is to show that if $\Gamma \nvdash A$, then the set:
$$
\Gamma \cup \{¬A\}
$$
is syntactically consistent, and from such a consistent set one can construct a valuation that makes every formula in $\Gamma$ true while making $A$ false.

Such a valuation is a counterexample to:
$$
\Gamma \models A
$$

Therefore, if:
$$
\Gamma \models A
$$
then no such counterexample exists, and hence:
$$
\Gamma \vdash A
$$

### Entailment and Unsatisfiability

Semantic consequence can also be expressed using unsatisfiability.

For any set of formulas $\Gamma$ and formula $A$:
$$
\Gamma \models A
$$
if and only if:
$$
\Gamma \cup \{¬A\}
$$
is unsatisfiable.

To see this, suppose first that $\Gamma \models A$. Then every valuation satisfying $\Gamma$ also satisfies $A$, so no valuation can satisfy both $\Gamma$ and $¬A$.

Conversely, suppose $\Gamma \cup \{¬A\}$ is unsatisfiable. Then there is no valuation that satisfies all formulas in $\Gamma$ while making $A$ false. Hence every valuation satisfying $\Gamma$ must satisfy $A$, so:
$$
\Gamma \models A
$$

### Example 1.40

We show again that:
$$
\{p \to q, p\} \models q
$$

By the unsatisfiability criterion, it is enough to show that:
$$
\{p \to q, p, ¬q\}
$$
is unsatisfiable.

Assume a valuation $v$ satisfies all three formulas. Then:
$$
v(p \to q)=\mathrm{T}
$$
$$
v(p)=\mathrm{T}
$$
$$
v(¬q)=\mathrm{T}
$$

The last condition gives:
$$
v(q)=\mathrm{F}
$$

But if $p$ is true and $q$ is false, then:
$$
v(p \to q)=\mathrm{F}
$$

This contradicts the assumption that:
$$
v(p \to q)=\mathrm{T}
$$

Therefore no such valuation exists, and the set is unsatisfiable.

### Role of the Theorem

Soundness gives reliability. It says that a formal proof cannot lead from true assumptions to a false conclusion.

Completeness gives adequacy. It says that the proof rules are sufficient to derive every conclusion that follows semantically from the assumptions.

Together, the two properties justify the use of formal derivations as a complete method for reasoning about propositional truth.