We now want to show that whenever then also Combined with the soundness Theorem 22, this shows that the notions of provable and true coincide for propositional logic, just as they did for the tree system. The examples above should hint at how flexible and useful this result actually is. This will be even more evident for first order (predicate) logic.
Theorem 26 (Completeness) For any theory and any formula if then
Proof: We prove this by verifying that if is formally consistent, then it is satisfiable. To see that this gives the result, suppose that Then is unsatisfiable, and it would therefore follow that is formally inconsistent. Thus and therefore
Suppose then that is a given formally consistent theory. By Corollary 13, we may assume that is also complete, i.e., that for any formula either or Consider the valuation
where is the characteristic function of i.e., iff We claim that
To prove this, we require one additional result about the provability relation
Proof: To show that it suffices to see that By proof by contrapositive, it is enough to show that and for this it suffices to see that By the deduction theorem, one only needs to check that But this is clear, since this set is formally inconsistent.
Similarly, by proof of contrapositive, to see that it suffices to see that but this is clear.
We now proceed to prove that for as above. We check for all formulas by induction on the length of a parsing sequence for that iff
Since is complete and this holds for a propositional variable.
Assuming the result for it follows immediately for by completeness of
Finally, assume the result for both and and we need to show that it also holds for We need to prove that iff or equivalently, that iff or, what is the same, and By the induction hypothesis, this is equivalent to saying that and
This is finally what we prove: iff and
Assume first that and Then If then and therefore is formally inconsistent.
Conversely, suppose that Then By Lemma 27, so and and we are done.
Corollary 28 There is an algorithm that on input where is a finite set of formulas, and is a formula, decides whether
On the other hand, the question of how efficient such an algorithm is, turns out to be much more complicated (it is equivalent to the P vs NP problem.)
12. Additional connectives
All the results above hold even if we allow additional connectives in the language, modulo a suitable extension of the propositional axioms. (Some of the proofs need minor modifications, such as the argument for unique readability.) It is a useful exercise to see that if we allow the standard connectives in addition to then, by extending the propositional axioms as follows, we can recover the completeness theorem:
Typeset using LaTeX2WP. Here is a printable version of this post.