Now that we have a formal system for arithmetic we can do what we discussed earlier and show that the set of theorems is arithmetic. If we’ve already done this for first order logic, which I haven’t but I did mention that this can be done, it’s not even particularly difficult. The axioms and the first rule of inference present no problems. The second rule of inference is more complicated but recognising instances of this rule is essentially a matter of pattern matching, and we’ve seen how to do pattern matching within arithmetic. Not every theorem is a sentence, but recognising which ones are is also a pattern matching problem and so the set of sentences which are theorems is also arithmetic.
Tarski’s theorem, that true sentences are not an arithmetic set, is interesting in itself, but it’s particularly interesting in combination with the observation that the set of provable sentences is arithmetic. This leads to the conclusion, first proved by Kurt Gödel, that these two sets are not the same, i.e. that there must either be a sentence which is true but cannot be proved, or a sentence which is false but can be proved!
The formulation above is somewhat sloppy. For simplicity I’ve referred to sets of sentences as being arithmetic or not, but arithmeticity is a property which applies to sets of natural numbers rather than sentences. What I really mean is that the sets of encodings of those sentences are arithmetic or not. But the set of encodings determines the set of sentences uniquely, so if the sets of encodings are different then so are the sets of sentences. So our final conclusion doesn’t reference the encodings.
If this were restricted to the formal system above then it wouldn’t have much interest. After all, the precise formal system above appears in these notes and nowhere else, so finding out that it’s incapable of proving all true statements in arithmetic isn’t terribly interesting. Perhaps I just need to add a new axiom or strengthen one of the rules of inference? The argument that led us to this point is quite a general one, though. Tarski’s theorem didn’t depend on the choice of formal system at all. The proof that theorems are an arithmetic set didn’t use any properties of this particular formal system. I haven’t defined the notion of a formal system precisely, but under any definition in which we can mechanically check whether proofs are valid we will get the same conclusion. So Gödel’s theorem is not a theorem about a particular formal system for arithmetic but rather a theorem about all possible formal systems for arithmetic.