Rosser’s theorem

Gödel did not prove his theorem as a consequence of Tarski’s theorem, which wasn’t proved until a couple of years later. In fact Tarski’s proof of his theorem was inspired by Gödel’s proof of his.

One way to think about Gödel’s theorem is that it says a formal system for arithmetic can be sound or semantically complete, but not both. Equivalently, every sound system is semantically incomplete. A sound system which is semantically complete is syntactically complete, so an alternate approach would be to prove first that every sound system is syntactically incomplete, and then derive semantic incompleteness as a result. This is roughly what Gödel tried to do. What he got wasn’t quite syntactic incompleteness but was sufficient to prove semantic incompleteness. A few years after Tarski proved his theorem Barkley Rosser succeeded in constructing a proof along the lines which Gödel had initially attempted, showing that a system for arithmetic can be consistent or syntactically complete, but not both. The main interest of this result is that the interpretation of the system now plays only a very minor role, since consistency and syntactic completeness require from the interpretation only a concept of negation. The interpretation is still lurking in one other place though. For any of these theorems to apply we need a certain level of descriptive completeness of our system; it has to be capable of describing enough of elementary arithmetic to be able to carry out an encoding in such a way that concatenation is representable within the system.

One final historical note is that Gödel’s first goal was not to prove any of the theorems mentioned above but rather to prove that Peano arithmetic is inconsistent! We now know that it’s at most consistent or complete but we don’t know which. Most logicians and mathematicians assume it’s consistent and therefore not complete, which is why Gödel’s theorem is referred to as Gödel’s first incompleteness theorem–there is also a second theorem–rather than Gödel’s first inconsistency theorem. We could be wrong though. Gödel himself, at least at some point, must have thought that we were or he wouldn’t have set out to prove inconsistency. Gödel was very clever so even though he didn’t actually succeed in proving Peano arithmetic’s inconsistency we should perhaps be more cautious in assuming its consistency.