Section 09: Soundness and completeness

This toolkit is incredibly convenient. It is also intuitive, because it seems natural that provability and semantic entailment should agree. Yet, do not be fooled by the similarity of the symbols ‘⊨’ and ‘⊢ .’ The fact that these two are really interchangeable is not a simple thing to prove.

Why should we think that an argument that can be proven is necessarily a valid argument? That is, why think that \(\mathcal{A}\) ⊢ \(\mathcal{B}\) implies \(\mathcal{A}\) ⊨ \(\mathcal{B}\)?

This is the problem of soundness. A proof system is sound if there are no proofs of invalid arguments. Demonstrating that the proof system is sound would require showing that any possible proof is the proof of a valid argument. It would not be enough simply to succeed when trying to prove many valid arguments and to fail when trying to prove invalid ones.

Fortunately, there is a way of approaching this in a step-wise fashion. If using the &E rule on the last line of a proof could never change a valid argument into an invalid one, then using the rule many times could not make an argument invalid. Similarly, if using the &E and ∨E rules individually on the last line of a proof could never change a valid argument into an invalid one, then using them in combination could not either.

The strategy is to show for every rule of inference that it alone could not make a valid argument into an invalid one. It follows that the rules used in combination would not make a valid argument invalid. Since a proof is just a series of lines, each justified by a rule of inference, this would show that every provable argument is valid.

Consider, for example, the &I rule. Suppose we use it to add \(\mathcal{A}\)&\(\mathcal{B}\) to a valid argument. In order for the rule to apply, \(\mathcal{A}\) and \(\mathcal{B}\) must already be available in the proof. Since the argument so far is valid, \(\mathcal{A}\) and \(\mathcal{B}\) are either premises of the argument or valid consequences of the premises. As such, any model in which the premises are true must be a model in which \(\mathcal{A}\) and \(\mathcal{B}\) are true. According to the definition of truth in ql, this means that \(\mathcal{A}\)&\(\mathcal{B}\) is also true in such a model. Therefore, \(\mathcal{A}\)&\(\mathcal{B}\) validly follows from the premises. This means that using the &E rule to extend a valid proof produces another valid proof.

In order to show that the proof system is sound, we would need to show this for the other inference rules. Since the derived rules are consequences of the basic rules, it would suffice to provide similar arguments for the 16 other basic rules. This tedious exercise falls beyond the scope of this book.

Given a proof that the proof system is sound, it follows that every theorem is a tautology.

It is still possible to ask: Why think that every valid argument is an argument that can be proven? That is, why think that \(\mathcal{A}\) ⊨ \(\mathcal{B}\) implies \(\mathcal{A}\) ⊢ \(\mathcal{B}\)?

This is the problem of completeness. A proof system is complete if there is a proof of every valid argument. Completeness for a language like QL was first proven by Kurt Gödel in 1929. The proof is beyond the scope of this book.

The important point is that, happily, the proof system for QL is both sound and complete. This is not the case for all proof systems and all formal languages. Because it is true of QL, we can choose to give proofs or construct models— whichever is easier for the task at hand.

Summary of definitions

• A sentence A is a theorem if and only if ⊢\(\mathcal{A}\).
• Two sentences \(\mathcal{A}\) and \(\mathcal{B}\) are provably equivalent if and only if \(\mathcal{A}\)⊢\(\mathcal{B}\) and \(\mathcal{B}\)⊢\(\mathcal{A}\).
• {\(\mathcal{A}\)₁,\(\mathcal{A}\)₂,...} is provably inconsistent if and only if, for some sentence \(\mathcal{B}\), {\(\mathcal{A}\)₁,\(\mathcal{A}\)₂,...}⊢(\(\mathcal{B}\) &¬\(\mathcal{B}\)).