I’ve already mentioned that formal languages described by phrase structure grammars have encodings which are arithmetic sets. If we have axioms and rules of inference as well then we can look at the sublanguage consisting of theorems in this formal system. The set of the encodings of theorems also turns out to be arithmetic. This is a theorem of Gödel. The word “theorem” is used in different senses in the two preceding sentences. In the first of them it means a statement with a formal proof and in the second it means a statement with an informal proof. Gödel’s theorem applies to Peano arithmetic, but is more general than that.
With an interpretation which enables us to characterise statements as true of false we can also look at the sublanguage of true statements. In particular we can consider the encodings of true statements in Peano arithmetic. This set is not arithmetic. That is a theorem of Tarski.
Gödel’s theorem is based on the insight that it’s not only possible, as we’ve already discussed, to make statements about Peano arithmetic within Peano arithmetic but it’s even possible to construct statements in Peano arithmetic which refer to themselves. In essence you can create statements with interpretations like “I cannot be proved” or “if I can be proved then I can also be disproved”. The first of these sentences is roughly the one at the heart of Gödel’s argument. The second is used in a strengthened version of that theorem due to Rosser.
Combining the theorems of Gödel and Tarski we see that the set of theorems in Peano arithmetic and the set of true statements cannot be the same set. The situation is even worse than it appears though. This is not simply a problem with a particular formal system for arithmetic, which we might hope to fix by, for example, adding a missing axiom or rule of inference. Gödel’s theorem is not specific to a particular formal system but applies to any formal system. Tarski’s theorem doesn’t even mention formal systems. It is purely a statement about the language of true statements. So no matter what replacement formal system we consider for arithmetic the set of true statements and theorems will always be different.
The combination of Gödel and Tarski tells us there must be a true statement which is not a theorem or a theorem which is not a true statement. There could also be both. The theorems don’t provide any insight into which of these possibilities occurs. A false theorem would be much more damaging than a true but unprovable statement. Most mathematicians and logicians believe that all theorems in Peano arithmetic are true but that there are true statements which are not theorems. In other words, they believe the system is sound but incomplete. Other than the fact that no one has yet found a contradiction there is no actual evidence for this belief. Gödel himself was skeptical of the soundness of arithmetic. His theorem was the result of an ultimately unsuccessful attempt to prove the inconsistency of Peano arithmetic.
Although he didn’t succeed in proving the inconsistency of arithmetic Gödel did succeed in killing the project, dating back to Euclid, of fully axiomatising all of mathematics. Gödel’s work is generally remembered in connection with Peano arithmetic but in fact he considered two axiomatic theories which seemed like candidates for the axiomatisation of mathematics. One was Peano arithmetic and the other was axiomatic set theory, which is our next topic.