Formal Logic

6. Correctness and completeness

6.1. Correctness

So far, we have defined two notions that allow formulas "of interest" to be distinguished from other formulas: the semantic notion of validity and the syntactic notion of provability. Intuitively, a valid formula stands for a proposition that is semantically true, and a provable formula stands for a proposition that can be proved to be true. We expect, of course, these two notions to be related. Indeed, an axiomatic system that would make it possible to prove propositions that are not valid should be considered as incorrect. Conversely, if there would be propositions that are semantically true but that cannot be proved, then the axiomatic system should be considered to be incomplete. We start by proving the correctness theorem that states that every provable formula is valid.

Let $α$ be a formula. If $⊢ α$ then $⊨ α$.

The proof proceeds by induction on the definition of a provable formula.

$⊢ α$ because $α$ is an axiom.
We have to check that each axiom of Definition 7 is indeed valid. This has been done in Exercice 3.

$⊢ α$ is obtained as the conclusion of an inference rule.

In this case, there exists a formula $β$ such that the derivation of $α$ ends up as follows:


⋮		⋮
$β$		$β → α$

$α$

By induction hypothesis, $⊨ β$ and $⊨ β → α$, that is, for every model $\sc M$, $⟦β⟧^{\sc M} = 1$ and $⟦β → α⟧^{\sc M} = 1$. We then establish the validity of $α$ as follows:

$⟦α⟧^{\sc M}$	$=$	$0+⟦α⟧^{\sc M}$
	$=$	$1↖{-}+⟦α⟧^{\sc M}$
	$=$	$\ov{⟦β⟧}^{\sc M}+⟦α⟧^{\sc M}$	(by induction hypothesis)
	$=$	$⟦β→α⟧^{\sc M}$	(by Definition 4)
	$=$	$1$	(by induction hypothesis)

6.2. Theories

In establishing the equivalence between validity and provability, Proposition 7 is the easy part. Proving the converse, i.e., establishing the completeness theorem, is much more involved and will occupy the remainder of the present chapter.

A few definitions are in order.

A theory is defined to be a set of formulas.

A theory is therefore just another name for a set of formulas. Consequently, if $Σ$ is such a set of formulas, Definition 10 also defines the notion of provability under a theory $Σ$. This allows the notions of a consistent theory and of complete theory to be defined.

A theory $Σ$ is said to be consistent if and only if there is no formula $α$ such that $Σ ⊢ α$ and $Σ ⊢ ¬α$.

A theory $Σ$ is said to be complete if and only if for evey formula $α$ either $Σ ⊢ α$ or $Σ ⊢ ¬α$.

In definition 13, nothing prevents a theory to be an infinite set of formulas. Definitions 14 and 15 still make sense in such a case because it is not stipulated in Definition 10 that the set of formulas $Γ$ must be finite. Nevertheless, since derivations are finite objects, in case $Σ ⊢ α$, there exists a finite subset $Γ ⊂ Σ$ such that $Γ ⊢ α$. Taking this remark into account, the notion of a consistent theory, for instance, may be rephrased as follows. A theory $Σ$ is said to be consistent if and only if there is no finite subset $Γ ⊂ Σ$ and no formula $α$ such that $Γ ⊢ α$ and $Γ ⊢ ¬α$.

Given two theories $Σ_0$ and $Σ_1$, one says that $Σ_1$ extends $Σ_0$ in case everything which is provable under $Σ_0$ is also provable under $Σ_1$. This is stated by the next definition.

Let $Σ_0$ and $Σ_1$ be two theories. $Σ_1$ is said to be an extension of $Σ_0$ if and only if for every formula $α$ such that $Σ_0 ⊢ α$ it is the case that $Σ_1 ⊢ α$.

Finally, one defines a model of a theory to be a model that satisfies all the formulas that are provable under the theory.

Let $Σ$ be a theory, and $\sc M$ be a model. $\sc M$ is a model of $Σ$ if and only if for every formula $α$ such that $Σ ⊢ α$ one has that $⟦α⟧^{\sc M} = 1$.

Alternatively, one could have defined a model of a theory to be a model that satisfies all the formulas that belong to the theory. Then, one would have to establish that this alternative definition is equivalent to Definition 17. This can be done by using a proof similar to the one of Proposition 7.

6.3. Lindenbaum's lemma

In this section, we state and prove an important proposition known as Lindenbaum's lemma. It says that every consistent theory can be extended to a complete consistent theory. We start by establishing a technical lemma.

Let $Σ$ be a theory, and $α$ be a formula. If it is not the case that $Σ ⊢ ¬ α$ then $Σ ∪ \{α\}$ is consistent.

Suppose, by way of contradiction, that $Σ ∪ \{α\}$ is not consistent. Then, by definition, there exists a formula $β$ such that

$Σ, α ⊢ ¬ β$ and $Σ, α ⊢ β$

Then, by Rule ($¬$-elim) of Definition 11, we have:

$Σ, α ⊢ ⊥$

But then, by Rule ($¬$-intro) of Definition 11:

$Σ ⊢ ¬ α $

which contradicts the hypothesis.

We are now in a position of stating and proving Lindenbaum's lemma.

If a theory$ Σ$ is consistent, then there exists a complete consistent theory that extends $Σ$.

We construct a theory $Σ_ω$ that extends $Σ$ and we show that it is consistent and complete.

Let $α_0, α_1, α_2, ...$ be an enumeration of all the formulas, and define the following sequence of theories:

$ \table Σ_0, =, Σ\text' '; Σ_{i+1}, =, {\{\table Σ_i\text' ', \text'if ' Σ_i ⊢ ¬ α_i; Σ_i ∪ \{α_i\}, \text'otherwise '} $

Then define $Σ_ω$ as follows:

$Σ_ω = ⋃_{i ∈ ℕ} Σ_i$

Clearly, $Σ_ω$ is an extension of $Σ$, and it remains to prove that it is both consistent and complete.

In order to show that $Σ_ω$ is consistent, we first establish the consistency of each theory $Σ_i$, by induction on the natural numbers. For the base case, we have that $Σ_0$ is $Σ$, which is consistent by hypothesis. For the inductive step, assume that $Σ_i$ is consistent. Then, if $Σ_i ⊢ ¬ α_i$, we have that $Σ_{i+1}$ is $Σ_i$, which is consistent by induction hypothesis. Otherwise, $Σ_{i+1}$ is $Σ_i ∪ \{α_i\}$, which is consistent by Lemma 8.

Now assume, by way of contradiction, that $Σ_ω$ is not consistent. This means that there exists a formula $α$ such that $Σ_ω ⊢ α$ and $Σ_ω ⊢ ¬ α$. Since derivations are finite, it implies that there exists a finite set of formulas, $Γ⊂Σ_ω$, such that $Γ ⊢ α$ and $Γ ⊢ ¬ α$. But then, there must exist $k ∈ ℕ$ such that $Γ⊂Σ_k$. Hence, there would exist $k ∈ ℕ$ such that $Σ_k ⊢ α$ and $Σ_k ⊢ ¬ α$. But this contradicts the fact that each theory $Σ_i$ is consistent.

In order to show that $Σ_ω$ is complete, take an arbitrary formula $α$. This formula must appear, at some point, in the enumeration. In other words, there exists $k ∈ ℕ$ such that $α = α_k$. Now, if $Σ_k ⊢ ¬ α_k$, we have that $Σ_ω ⊢ ¬ α$ because $Σ_k ⊂ Σ_ω$ and $α_k = α$. In the other case, we have that $Σ_{k+1} = Σ_k ∪ \{α_k\}$. Hence, $Σ_{k+1} ⊢ α_k$, which implies that $Σ_ω ⊢ α$. Therefore, for any arbitrary formula $α$, either $Σ_ω ⊢ α$ or $Σ_ω ⊢ ¬ α$.

6.4. Completeness

A key ingredient in the proof of the completeness theorem is the property that every consistent theory admits a model. In order to prove it, we first give a way of building models from theories.

Let $Σ$ be a theory. The model associated to $Σ$ is the model $\sc M$ such that for every $a ∈ {\sc A}$, $\sc M(a) = 1$ if and only if $Σ ⊢ a$.

The above construction is particularly interesting when $Σ$ is a complete consistent theory. In this case, the model $\sc M$ associated to $Σ$ is such that for every $a ∈ {\sc A}$, $\sc M(a) = 0$ if and only if $Σ ⊢ ¬ a$. Indeed, if $Σ ⊢ ¬ a$, it cannot be the case that $Σ ⊢ a$, because $Σ$ is consistent. Therefore, by definition of $\sc M$, $\sc M(a) ≠ 1$, which implies that $\sc M(a) = 0$. Conversely, if $\sc M(a) = 0$, by definition of $\sc M$, it is not the case that $Σ ⊢ a$. Consequently, we must have that $Σ ⊢ ¬ a$, because $Σ$ is complete.

What is the model associated to an inconsistent theory?

If a theory $Σ$ is not consistent, there exists a formula $α$ such that $Σ ⊢ α$ and $Σ ⊢ ¬ α$. Then, by Rule ($¬$-elim), we have: $Σ ⊢ ⊥$. Hence, by rule ($⊥$-elim), $Σ ⊢ β$ for every possible formula $β$. In particular, this holds for every atomic formula. Therefore, the model associated to an inconsistent theory is the model $\sc M$ such that for every $a ∈ {\sc A}$, $\sc M(a) = 1$.

The next lemma sheds light on the link between a complete consistent theory and its associated model.

Let $Σ$ be a complete consistent theory, and $\sc M$ be its associated model. The two following statements hold for every formula $α$ :

if $⟦α⟧^{\sc M} = 1$ then $Σ ⊢ α$
if $⟦α⟧^{\sc M} = 0$ then $Σ, α ⊢ ⊥$

The proof proceeds by induction on the definition of a formula.

$α = a$, for some $a ∈ \sc A$.

If $⟦a⟧^{\sc M} = 1$, then we have that $Σ ⊢ a$, by definition of ${\sc M}$.

If $⟦a⟧^{\sc M} = 0$, then we have that $Σ ⊢ ¬a$, because $Σ$ is complete. we may then conclude using (weakening), (identity), and ($¬$-elim):


$Σ ⊢ ¬ a$

$Σ, a ⊢ ¬ a$		$Σ, a ⊢ a$

$Σ, a ⊢ ⊥$

$α = \text'⊥'$.
1. This case holds vacuously.
2. We have that $Σ, ⊥ ⊢ ⊥$, by ($⊥$-left).
$α = \text'⊤'$.
1. We have that $Σ ⊢ \text'⊤'$, by ($⊤$-right).
2. This case holds vacuously.
$α = ¬α_1$, for some formula $α_1$.
1. If $⟦¬α_1⟧^{\sc M} = 1$, we have that $⟦α_1⟧^{\sc M} = 0$. Then, by induction hypothesis, $Σ, α_1 ⊢ ⊥$, and we may conclude using ($¬$-right):
  
  $Σ, α_1 ⊢ \text'⊥'$
  
  $Σ ⊢ ¬α_1$
2. If $⟦¬α_1⟧^{\sc M} = 0$, we have that $⟦α_1⟧^{\sc M} = 1$. Then, by induction hypothesis, $Σ ⊢ α_1 $, and we are done using ($¬$-left):
  
  $Σ ⊢ α_1$
  
  $Σ, ¬α_1 ⊢ ⊥$
$α = α_1∧α_2$, for some formulas $α_1$ and $α_2$.
1. If $⟦α_1∧α_2⟧^{\sc M} = 1$, we have that $⟦α_1⟧^{\sc M} =1$ and $⟦α_2⟧^{\sc M} =1$. Then, by induction hypothesis, $Σ ⊢ α_1$ and $Σ ⊢ α_2$. We conclude using ($∧$-right):
  
  $Σ ⊢ α_1$ $Σ ⊢ α_2$
  
  $Σ ⊢ α_1 ∧ α_2$
2. If $⟦α_1∧α_2⟧^{\sc M} = 0$, we have that $⟦α_1⟧^{\sc M} =0$ or $⟦α_2⟧^{\sc M} =0$. Suppose that $⟦α_1⟧^{\sc M} =0$. Then, by induction hypothesis, $Σ, α_1 ⊢ ⊥$, and we may conclude using ($∧$-left-1):
  
  $Σ, α_1 ⊢ ⊥$
  
  $Σ, α_1 ∧ α_2 ⊢ ⊥$
  
  The case where $⟦α_2⟧^{\sc M} =0$ is handled similarly, using ($∧$-left-2).
$α = α_1∨α_2$, for some formulas $α_1$ and $α_2$.
1. If $⟦α_1∨α_2⟧^{\sc M} = 1$, we have that $⟦α_1⟧^{\sc M} =1$ or $⟦α_2⟧^{\sc M} =1$. Suppose that $⟦α_1⟧^{\sc M} =1$. Then, by induction hypothesis, $Σ ⊢ α_1$, and we may conclude using ($∨$-right-1):
  
  $Σ ⊢ α_1$
  
  $Σ ⊢ α_1 ∨ α_2$
  
  The case where $⟦α_2⟧^{\sc M} =1$ is handled similarly, using ($∨$-right-2).
2. If $⟦α_1∨α_2⟧^{\sc M} = 0$, we have that $⟦α_1⟧^{\sc M} =0$ and $⟦α_2⟧^{\sc M} =0$. Then, by induction hypothesis, $Σ, α_1 ⊢ ⊥$ and $Σ, α_2 ⊢ ⊥$. We conclude using ($∨$-left):
  
  $Σ, α_1 ⊢ ⊥$ $Σ, α_2 ⊢ ⊥$
  
  $Σ, α_1 ∨ α_2 ⊢ ⊥$
$α = α_1→α_2$, for some formulas $α_1$ and $α_2$.
1. If $⟦α_1→α_2⟧^{\sc M} = 1$, we have that $⟦α_1⟧^{\sc M} =0$ or $⟦α_2⟧^{\sc M} =1$. We consider the two cases separetely. The first case is when $⟦α_1⟧^{\sc M} =0$. Then, by induction hypothesis, $Σ, α_1 ⊢ ⊥$, and we are done using ($⊥$-elim) and ($→$-right):
  
  $Σ, α_1 ⊢ ⊥$
  
  $Σ, α_1 ⊢ α_2$
  
  $Σ ⊢ α_1 → α_2$
  
  The second case is when $⟦α_2⟧^{\sc M} =1$. Then, by induction hypothesis, $Σ ⊢ α_2$, and we conclude using (weakening) and ($→$-right):
  
  $Σ ⊢ α_2$
  
  $Σ, α_1 ⊢ α_2$
  
  $Σ ⊢ α_1 → α_2$
2. If $⟦α_1→α_2⟧^{\sc M} = 0$, we have that $⟦α_1⟧^{\sc M} =1$ and $⟦α_2⟧^{\sc M} =0$. By induction hypothesis, $Σ ⊢ α_1$ and $Σ, α_2 ⊢ ⊥$. Then, we are done by ($→$-left):
  
  $Σ ⊢ α_1$ $Σ, α_2 ⊢ ⊥$
  
  $Σ, α→ α_2 ⊢ ⊥$

As an immediate consequence of the above lemma, we obtain that every complete consistent theory has a model.

Every complete consistent theory admits a model.

Let $Σ$ be a complete consistent theory, and $\sc M$ be its associated model. We show that $\sc M$ is indeed a model of $Σ$.

Suppose by way of contradiction that it is not the case and that, therefore, there exists a formula $α$ such that $Σ ⊢ α$ and $⟦α⟧^{\sc M} = 0$. But then, by Lemma 10, we have that $Σ, α ⊢ ⊥$. This implies, by ($¬$-intro), that $Σ ⊢ ¬ α$, which contradicts the consistency of $Σ$.

By combining Lindebaum's lemma and the above corollary, we obtain the key result we were expecting.

Every consistent theory admits a model.

Let $Σ$ be a consistent theory. By Lemma 9, there exists a complete consistent theory $Σ_ω$ that extends $Σ$. By Corollary 11, $Σ_ω$ admits a model $\sc M$. Then, $\sc M$ is also a model of $Σ$ since $Σ_ω$ is an extension of $Σ$.

We are finally in a position of proving the completeness theorem.

Let $α$ be a formula. If $⊨ α$ then $⊢ α$.

Suppose, by way of contradiction, that is not the case that $⊢ α$. Since $⊢ ¬¬α→α$, it is not the case either that $⊢ ¬¬α$. Then, by Lemma 8, $\{¬α\}$ is a consistent theory. Therefore, by Proposition 12, there exists a model $\sc M$ such that $⟦¬α⟧^{\sc M} = 1$. Then, by Definition 4, $⟦α⟧^{\sc M} = 0$, which contradicts that $⊨ α$.

$Σ, α_1 ⊢ ⊥$		$Σ, α_2 ⊢ ⊥$

$Σ, α_1 ∨ α_2 ⊢ ⊥$