Although we have proven some useful completeness theorems about the proof systems in the last two chapters, we have not been able to prove absolute completeness: that every valid sequent is derivable. Because of some formal incompleteness results, we will never be able to prove such a completeness theorem, for any finitary proof system; but there are several ways in which we can, at least partially, escape the effect of these incompleteness results. In this chapter, I present the incompleteness theorems and some of the partial solutions.

There are two main incompleteness results, as discussed in the first section below. The first says that we will never be able to derive all valid closed sequents which have signed formulae in negative contexts, and follows from the non-existence of a solution to the Halting Problem. (We can deal with many of the important cases of this result by adding extra rules which I will describe.) The second result says that we will never be able to derive all valid sequents with free variables, even if they have no signed formulae in negative contexts, and is a version of Gödel's Incompleteness Theorem.

The “mathematical” solution to these problems is to bring the proof theory closer to a kind of model theory, by allowing infinitary elements into the proof systems. Though these are not adequate solutions for practical theorem proving, they are useful in that they shed light on the extent to which the proof systems in question are complete.