Soundness and Completeness

Editorial

This chapter collects soundness and completeness results for propositional intuitionistic logic. It needs an introduction. The completeness proof makes use of facts about provability that should be stated and proved explicitly somewhere.

Editorial

The soundness proof relies on the fact that all axioms are intuitionistically valid; this still needs to be proved, e.g., in the Semantics chapter.

Soundness theorem for the intuitionistic axiomatic calculus

[Soundness] If $\Gamma \Proves !A$source, then $\Gamma \Entails !A$source.

Proof

We prove that if $\Gamma \Proves !A$source, then $\Gamma \Entails !A$source. The proof is by induction on the number $n$source of formulas in the derivation of $!A$source from $\Gamma$source. We show that if $!A_1$source, dots, $!A_n = !A$source is a derivation from $\Gamma$source, then $\Gamma \Entails !A_n$source. Note that if $!A_1$source, dots, $!A_n$source is a derivation, so is $!A_1$source, dots, $!A_k$source for any $k<n$source.

There are no derivations of length $0$source, so for $n=0$source the claim holds vacuously. So the claim holds for all derivations of length $<n$source. We distinguish cases according to the justification of $!A_n$source.

1. $!A_n$source is an axiom. All axioms are valid, so $\Gamma \Entails !A_n$source for any $\Gamma$source.

2. $!A_n \in \Gamma$source. Then for any $\mModel{M}$source and $w$source, if $\mSat{M}{\Gamma}[w]$source, obviously $\mSat{M}{!A_n}[w]$source, i.e., $\Gamma \Entails !A$source.

3. $!A_n$source follows by MP from $!A_i$source and $!A_j \ident !A_i \lif !A_n$source. $!A_1$source, dots, $!A_i$source and $!A_1$source, dots, $!A_j$source are derivations from $\Gamma$source, so by inductive hypothesis, $\Gamma \Entails !A_i$source and $\Gamma \Entails !A_i \lif !A_n$source.

   Suppose $\mSat{M}{\Gamma}[w]$source. Since $\mSat{M}{\Gamma}[w]$source and $\Gamma \Entails !A_i \lif !A_n$source, $\mSat{M}{!A_i \lif !A_n}[w]$source. By definition, this means that for all $w'$source such that $Rww'$source, if $\mSat{M}{!A_i}[w']$source then $\mSat{M}{!A_n}[w']$source. Since $R$source is reflexive, $w$source is among the $w'$source such that $Rww'$source, i.e., we have that if $\mSat{M}{!A_i}[w]$source then $\mSat{M}{!A_n}[w]$source. Since $\Gamma \Entails !A_i$source, $\mSat{M}{!A_i}[w]$source. So, $\mSat{M}{!A_n}[w]$source, as we wanted to show.

Soundness theorem for intuitionistic natural deduction

[Soundness] If $\Gamma \Proves !A$source, then $\Gamma \Entails !A$source.

Proof

We prove that if $\Gamma \Proves !A$source, then $\Gamma \Entails !A$source. The proof is by induction on the derivation of $!A$source from $\Gamma$source.

1. If the derivation consists of just the assumption $!A$source, we have $!A \Proves !A$source, and want to show that $!A \Entails !A$source. Suppose that $\mSat{M}{!A}[w]$source. Then trivially $\mSat{M}{!A}[w]$source.

2. The derivation ends in $\Intro{\land}$source: Exercise.

3. The derivation ends in $\Elim{\land}$source: Exercise.

4. The derivation ends in $\Intro{\lor}$source: Suppose the premise is $!B$source, and the undischarged assumptions of the derivation ending in $!B$source are $\Gamma$source. Then we have $\Gamma \Proves !B$source and by inductive hypothesis, $\Gamma \Entails !B$source. We have to show that $\Gamma \Entails !B \lor !C$source. Suppose $\mSat{M}{\Gamma}[w]$source. Since $\Gamma \Entails !B$source, $\mSat{M}{!B}[w]$source. But then also $\mSat{M}{!B \lor !C}[w]$source. Similarly, if the premise is $!C$source, we have that $\Gamma \Entails !C$source.

5. The derivation ends in $\Elim{\lor}$source: The derivations ending in the premises are of $!B \lor !C$source from undischarged assumptions $\Gamma$source, of $!D$source from undischarged assumptions $\Delta_1 \cup \{!B\}$source, and of $!D$source from undischarged assumptions $\Delta_2 \cup \{!C\}$source. So we have $\Gamma \Proves !B \lor !C$source, $\Delta_1 \cup \{!B\} \Proves !D$source, and $\Delta_2 \cup \{!C\} \Proves !D$source. By induction hypothesis, $\Gamma \Entails !B \lor !C$source, $\Delta_1 \cup \{!B\} \Entails !D$source, and $\Delta_2 \cup \{!C\} \Entails !D$source. We have to prove that $\Gamma \cup \Delta_1 \cup \Delta_2 \Entails !D$source.

   Suppose $\mSat{M}{\Gamma \cup \Delta_1 \cup \Delta_2}[w]$source. Then $\mSat{M}{\Gamma}[w]$source and since $\Gamma \Entails !B \lor !C$source, $\mSat{M}{!B \lor !C}[w]$source. By definition of $\mSat{M}{}$source, either $\mSat{M}{!B}[w]$source or $\mSat{M}{!C}[w]$source. So we distinguish cases: (a) $\mSat{M}{!B}[w]$source. Then$\mSat{M}{\Delta_1 \cup \{!B\}}[w]$source. Since $\Delta_1 \cup \{!B\} \Entails !D$source, we have $\mSat{M}{!D}[w]$source. (b) $\mSat{M}{!C}[w]$source. Then $\mSat{M}{\Delta_2 \cup \{!C\}}[w]$source. Since $\Delta_2 \cup \{!C\} \Entails !D$source, we have $\mSat{M}{!D}[w]$source. So in either case, $\mSat{M}{!D}[w]$source, as we wanted to show.

6. The derivation ends with $\Intro{\lif}$source concluding $!B\lif !C$source. Then the premise is $!C$source, and the derivation ending in the premise has undischarged assumptions $\Gamma \cup \{!B\}$source. So we have that $\Gamma \cup \{!B\} \Proves !C$source, and by induction hypothesis that $\Gamma \cup \{!B\} \Entails !C$source. We have to show that $\Gamma \Entails !B \lif !C$source.

   Suppose $\mSat{M}{\Gamma}[w]$source. We want to show that for all $w'$source such that $Rww'$source, if $\mSat{M}{!B}[w']$source, then $\mSat{M}{!C}[w']$source. So assume that $Rww'$source and $\mSat{M}{!B}[w']$source. By the earlier proposition that intuitionistic truth persists along accessibility, $\mSat{M}{\Gamma}[w']$source. Since $\Gamma \cup \{!B\} \Entails !C$source, $\mSat{M}{!C}[w']$source, which is what we wanted to show.

7. The derivation ends in $\Elim{\lif}$source and conclusion $!C$source. The premises are $!B \lif !C$source and $!B$source, with derivations from undischarged assumptions $\Gamma$source, $\Delta$source. So we have $\Gamma \Proves !B \lif !C$source and $\Delta \Proves !B$source. By inductive hypothesis, $\Gamma \Entails !B \lif !C$source and $\Delta \Entails !B$source. We have to show that $\Gamma \cup \Delta \Entails !C$source.

   Suppose $\mSat{M}{\Gamma \cup \Delta}[w]$source. Since $\mSat{M}{\Gamma}[w]$source and $\Gamma \Entails !B \lif !C$source, $\mSat{M}{!B \lif !C}[w]$source. By definition, this means that for all $w'$source such that $Rww'$source, if $\mSat{M}{!B}[w']$source then $\mSat{M}{!C}[w']$source. Since $R$source is reflexive, $w$source is among the $w'$source such that $Rww'$source, i.e., we have that if $\mSat{M}{!B}[w]$source then $\mSat{M}{!C}[w]$source. Since $\mSat{M}{\Delta}[w]$source and $\Delta \Entails !B$source, $\mSat{M}{!B}[w]$source. So, $\mSat{M}{!C}[w]$source, as we wanted to show.

8. The derivation ends in $\FalseInt$source, concluding $!A$source. The premise is $\lfalse$source and the undischarged assumptions of the derivation of the premise are $\Gamma$source. Then $\Gamma \Proves \lfalse$source. By inductive hypothesis, $\Gamma \Entails \lfalse$source. We have to show $\Gamma \Entails !A$source.

   We proceed indirectly. If $\Gamma \Entails/ !A$source there is a model $\mModel{M}$source and world $w$source such that $\mSat{M}{\Gamma}[w]$source and $\mSat/{M}{!A}[w]$source. Since $\Gamma \Entails \lfalse$source, $\mSat{M}{\lfalse}[w]$source. But that's impossible, since by definition, $\mSat/{M}{\lfalse}[w]$source. So $\Gamma \Entails !A$source.

9. The derivation ends in $\Intro\lnot$source: Exercise.

10. The derivation ends in $\Elim\lnot$source: Exercise.

Exercise completing the natural-deduction soundness proof

Complete the proof of the natural-deduction soundness theorem. For the cases for $\Intro\lnot$source and $\Elim\lnot$source, use the definition of $\mSat{M}{\lnot !A}[w]$source in the definition of truth at a world, i.e., don't treat $\lnot !A$source as defined by $!A \lif \lfalse$source.

Exercise giving three intuitionistic nonderivability results

Show that the following formulas are not derivable in intuitionistic logic:

1. $(!A \lif !B) \lor (!B \lif !A)$source

2. $(\lnot\lnot !A \lif !A) \lif (!A \lor \lnot !A)$source

3. $(!A \lif !B \lor !C) \lif \bigl((!A \lif !B)\lor(!A \lif !C)\bigr)$source

Definition of a prime set of formulas

A set of formulas $\Gamma$source is prime iff

1. $\Gamma$source is consistent, i.e., $\Gamma \Proves/ \lfalse$source;

2. if $\Gamma \Proves !A$source then $!A \in \Gamma$source; and

3. if $!A \lor !B \in \Gamma$source then $!A \in \Gamma$source or $!B \in \Gamma$source.

Lindenbaum's Lemma for intuitionistic logic

[Lindenbaum's Lemma] If $\Gamma \Proves/ !A$source, there is a $\Gamma^* \supseteq \Gamma$source such that $\Gamma^*$source is prime and $\Gamma^* \Proves/ !A$source.

Proof

Let $!B_1 \lor !C_1$source, $!B_2 \lor !C_2$source, dots, be an enumeration of all formulas of the form $!B \lor !C$source. We'll define an increasing sequence of sets of formulas $\Gamma_n$source, where each $\Gamma_{n+1}$source is defined as $\Gamma_n$source together with one new formula. $\Gamma^*$source will be the union of all $\Gamma_n$source. The new formulas are selected so as to ensure that $\Gamma^*$source is prime and still $\Gamma^* \Proves/ !A$source. This means that at each step we should find the first disjunction $!B_i \lor !C_i$source such that:

1. $\Gamma_n \Proves !B_i \lor !C_i$source

2. $!B_i \notin \Gamma_n$source and $!C_i \notin \Gamma_n$source

We add to $\Gamma_n$source either $!B_i$source if $\Gamma_n \cup \{!B_i\} \Proves/ !A$source, or $!C_i$source otherwise. We'll have to show that this works. For now, let's define $i(n)$source as the least $i$source such that the first condition selecting a disjunction and the second condition selecting a disjunction hold.

Define $\Gamma_0 = \Gamma$source and

If $i(n)$source is undefined, i.e., whenever $\Gamma_n \Proves !B \lor !C$source, either $!B \in \Gamma_n$source or $!C \in \Gamma_n$source, we let $\Gamma_{n+1} = \Gamma_n$source. Now let $\Gamma^* = \bigcup_{n=0}^\infty \Gamma_n$source

First we show that for all $n$source, $\Gamma_n \Proves/ !A$source. We proceed by induction on $n$source. For $n = 0$source the claim holds by the hypothesis of the theorem, i.e., $\Gamma \Proves/ !A$source. If $n>0$source, we have to show that if $\Gamma_n \Proves/ !A$source then $\Gamma_{n+1} \Proves/ !A$source. If $i(n)$source is undefined, $\Gamma_{n+1} = \Gamma_n$source and there is nothing to prove. So suppose $i(n)$source is defined. For simplicity, let $i = i(n)$source.

We'll prove the contrapositive of the claim. Suppose $\Gamma_{n+1} \Proves !A$source. By construction, $\Gamma_{n+1} = \Gamma_n \cup \{!B_i\}$source if $\Gamma_n \cup \{!B_i\} \Proves/ !A$source, or else $\Gamma_{n+1} = \Gamma_n \cup \{!C_i\}$source. It clearly can't be the first, since then $\Gamma_{n+1} \Proves/ !A$source. Hence, $\Gamma_n \cup \{!B_i\} \Proves !A$source and $\Gamma_{n+1} = \Gamma_n \cup \{!C_i\}$source. By definition of $i(n)$source, we have that $\Gamma _n \Proves !B_i \lor !C_i$source. We have $\Gamma_n \cup \{!B_i\} \Proves !A$source. We also have $\Gamma_{n+1} = \Gamma_n \cup \{!C_i\} \Proves !A$source. Hence, $\Gamma_n \Proves !A$source, which is what we wanted to show.

If $\Gamma^* \Proves !A$source, there would be some finite subset $\Gamma' \subseteq \Gamma^*$source such that $\Gamma' \Proves !A$source. Each $!D \in \Gamma'$source must be in $\Gamma_i$source for some $i$source. Let $n$source be the largest of these. Since $\Gamma_i \subseteq \Gamma_n$source if $i \le n$source, $\Gamma' \subseteq \Gamma_n$source. But then $\Gamma_n \Proves !A$source, contrary to our proof above that $\Gamma_n \Proves/ !A$source.

Lastly, we show that $\Gamma^*$source is prime, i.e., satisfies conditions the consistency condition in the definition of a prime set, the deductive-closure condition in the definition of a prime set, and the disjunction condition in the definition of a prime set of the definition of a prime set.

First, $\Gamma^* \Proves/ !A$source, so $\Gamma^*$source is consistent, so the consistency condition in the definition of a prime set holds.

We now show that if $\Gamma^* \Proves !B \lor !C$source, then either $!B \in \Gamma^*$source or $!C \in \Gamma^*$source. This proves the disjunction condition in the definition of a prime set, since if $!B \lor !C \in \Gamma^*$source then also $\Gamma^* \Proves !B \lor !C$source. So assume $\Gamma^* \Proves !B \lor !C$source but $!B \notin \Gamma^*$source and $!C \notin \Gamma^*$source. Since $\Gamma^* \Proves !B \lor !C$source, $\Gamma_n \Proves !B \lor !C$source for some $n$source. $!B \lor !C$source appears on the enumeration of all disjunctions, say, as $!B_j \lor !C_j$source. $!B_j \lor !C_j$source satisfies the properties in the definition of $i(n)$source, namely we have $\Gamma_n \Proves !B_j \lor !C_j$source, while $!B_j \notin \Gamma_n$source and $!C_j \notin \Gamma_n$source. At each stage, at least one fewer disjunction $!B_i \lor !C_i$source satisfies the conditions (since at each stage we add either $!B_i$source or $!C_i$source), so at some stage $m$source we will have $j = i(m)$source. But then either $!B \in \Gamma_{m+1}$source or $!C \in \Gamma_{m+1}$source, contrary to the assumption that $!B \notin \Gamma^*$source and $!C \notin \Gamma^*$source.

Now suppose $\Gamma^* \Proves !B$source. Then $\Gamma^* \Proves !B \lor !B$source. But we've just proved that if $\Gamma^* \Proves !B \lor !B$source then $!B \in \Gamma^*$source. Hence, $\Gamma^*$source satisfies the deductive-closure condition in the definition of a prime set of the definition of a prime set.

Exercise relating nonderivability of falsity to classical consistency

Show that if $\Gamma \Proves/ \bot$source then $\Gamma$source is consistent in classical logic, i.e., there is a valuation making all formulas in $\Gamma$source true.

Definition of the canonical intuitionistic model

Suppose $\Delta$source is prime. Then the canonical model $\mModel{M(\Delta)}$source for $\Delta$source is defined by:

1. $W = \Nat^*$source, the set of finite sequences of natural numbers.

2. $R$source is the partial order according to which $R\sigma\sigma'$source iff $\sigma$source is an initial segment of $\sigma'$source (i.e., $\sigma' = \sigma \concat \sigma''$source for some sequence $\sigma''$source).

3. $V(p) = \Setabs{\sigma}{p \in \Delta(\sigma)}$source.

Truth Lemma for the canonical model

If $\Delta$source is prime, then $\mSat{M(\Delta)}{!A}[\sigma]$source iff $\Delta(\sigma) \Proves !A$source.

Proof

By induction on $!A$source.

1. Case: $!A \ident \lfalse$source

   Since $\Delta(\sigma)$source is prime, it is consistent, so $\Delta(\sigma) \Proves/ \indfrm$source. By definition, $\mSat/{M(\Delta)}{\indfrm}[\sigma]$source.

2. Case: $!A \ident p$source

   By definition of $\mSat{{}}{}$source, $\mSat{M(\Delta)}{\indfrm}[\sigma]$source iff $\sigma \in V(p)$source, i.e., $\Delta(\sigma) \Proves \indfrm$source.

3. Case: $!A \ident \lnot !B$source

4. Case: $!A \ident !B \land !C$source

   $\mSat{M(\Delta)}{\indfrm}[\sigma]$source iff $\mSat{M(\Delta)}{!B}[\sigma]$source and $\mSat{M(\Delta)}{!C}[\sigma]$source. By induction hypothesis, $\mSat{M(\Delta)}{!B}[\sigma]$source iff $\Delta(\sigma) \Proves !B$source, and similarly for $!C$source. But $\Delta(\sigma) \Proves !B$source and $\Delta(\sigma) \Proves !C$source iff $\Delta(\sigma) \Proves \indfrm$source.

5. Case: $!A \ident !B \lor !C$source

   $\mSat{M(\Delta)}{\indfrm}[\sigma]$source iff $\mSat{M(\Delta)}{!B}[\sigma]$source or $\mSat{M(\Delta)}{!C}[\sigma]$source. By induction hypothesis, this holds iff $\Delta(\sigma) \Proves !B$source or $\Delta(\sigma) \Proves !C$source. We have to show that this in turn holds iff $\Delta(\sigma) \Proves \indfrm$source. The left-to-right direction is clear. The right-to-left direction follows since $\Delta(\sigma)$source is prime.

6. Case: $!A \ident !B \lif !C$source

   First the contrapositive of the left-to-right direction: Assume $\Delta(\sigma) \Proves/ !B \lif !C$source. Then also $\Delta(\sigma) \cup \{!B\} \Proves/ !C$source. Since $\tuple{!B, !C}$source is $\tuple{!B_n, !C_n}$source for some $n$source, we have $\Delta(\sigma.n) = (\Delta(\sigma) \cup \{!B\})^*$source, and $\Delta(\sigma.n) \Proves !B$source but $\Delta(\sigma.n) \Proves/ !C$source. By inductive hypothesis, $\mSat{M(\Delta)}{!B}[\sigma.n]$source and $\mSat/{M(\Delta)}{!C}[\sigma.n]$source. Since $R\sigma(\sigma.n)$source, this means that $\mSat/{M(\Delta)}{\indfrm}[\sigma]$source.

   Now assume $\Delta(\sigma) \Proves !B \lif !C$source, and let $R\sigma\sigma'$source. Since $\Delta(\sigma) \subseteq \Delta(\sigma')$source, we have: if $\Delta(\sigma') \Proves !B$source, then $\Delta(\sigma') \Proves !C$source. In other words, for every $\sigma'$source such that $R\sigma\sigma'$source, either $\Delta(\sigma') \Proves/ !B$source or $\Delta(\sigma') \Proves !C$source. By induction hypothesis, this means that whenever $R\sigma\sigma'$source, either $\mSat/{M(\Delta)}{!B}[\sigma']$source or $\mSat{M(\Delta)}{!C}[\sigma']$source, i.e., $\mSat{M(\Delta)}{\indfrm}[\sigma]$source.

Completeness theorem for intuitionistic logic

If $\Gamma \Entails !A$source then $\Gamma \Proves !A$source.

Proof

We prove the contrapositive: Suppose $\Gamma \Proves/ !A$source. Then by Lindenbaum's Lemma, there is a prime set $\Gamma^* \supseteq \Gamma$source such that $\Gamma^* \Proves/ !A$source. Consider the canonical model $\mModel{M(\Gamma^*)}$source for $\Gamma^*$source as defined in the definition of the canonical model. For any $!B \in \Gamma$source, $\Gamma^* \Proves !B$source. Note that $\Gamma^*(\emptyseq) = \Gamma^*$source. By the Truth Lemma (the Truth Lemma), we have $\mSat{M(\Gamma^*)}{!B}[\emptyseq]$source for all $!B \in \Gamma$source and $\mSat/{M(\Gamma^*)}{!A}[\emptyseq]$source. This shows that $\Gamma \Entails/ !A$source.

Exercise on formulas using only variables, disjunction, and conjunction

Show that if $!A$source only contains propositional variables, $\lor$source, and $\land$source, then $\Entails/ !A$source. Use this to conclude that $\lif$source is not definable in intuitionistic logic from $\lor$source and $\land$source.

Exercise proving the disjunction property

By using the completeness theorem prove that if $\Proves !A \lor !B$source then $\Proves !A$source or $\Proves !B$source. (Hint: Assume $\mSat/{M_1}{!A}$source and $\mSat/{M_2}{!B}$source and construct a new model $\mModel{M}$source such that $\mSat/{M}{!A \lor !B}$source.)

Exercise on linearly ordered relational models

Show that if $\mModel{M}$source is a relational model using a linear order then $\mSat{M}{(!A \lif !B)\lor(!B \lif !A)}$source.

Finite-countermodel theorem

If $\Entails/ !A$source then there is a finite model $\mSat/{M'}{!A}$source.

Proof

Assume $\mModel{M}=\tuple{W, R, V}$source is such that $\mSat/{M}{!A}$source and $P$source is the set of propositional variables occurring in $!A$source. Define $\mModel{M'}=\tuple{W', R', V'}$source by letting $W' = \Setabs{[w]}{w \in W}$source where $[w] = \Setabs{p \in P}{w \in V(p)}$source, $R'$source be the subset relation, and $V'(p)=\Setabs{[w]}{p \in [w]}$source. It should be clear that $W'$source is a finite set and that $\mModel{M'}$source is a relational model.

It can be shown, by induction on $!A$source, that

for all formulas $!A$source with only propositional variables from $P$source. This is left as an exercise for the reader.

Exercise finishing the finite-countermodel proof

Finish the proof of the finite-countermodel theorem by showing that $\mSat{M,w}{!A}$source iff $\mSat{M',[w]}{!A}$source for all formulas $!A$source with only propositional variables from $P$source.