Truth and provability, a thread. Let us compare Tarski's theorem on the nondefinability of truth with Gödel's incompleteness theorem. Smullyan advanced the view that much of the fascination with Gödel's theorem should be better directed toward Tarski's theorem.
Both theorems begin with the profound arithmetization idea, Gödel's realization that arithmetic interprets essentially any finite combinatorial process, including arithmetic syntax itself. Every arithmetic assertion φ is thus represented in arithmetic by Gödel code 'φ', a number.
Gödel's theorem (the first incompleteness theorem) is the claim that no computability axiomatizable true arithmetic theory can prove all arithmetic truths. Every such theory will admit true but unprovable assertions.
Tarski's theorem, in contrast, asserts that arithmetic truth is not arithmetically expressible. That is, there is no arithmetic predicate T(x) holding exactly of the codes of true assertions. There is no such expression T for which φ⇔T('φ') holds of every arithmetic assertion φ.
Tarski's theorem immediately implies Gödel's incompleteness theorem, since provability in a theory is arithmetically expressible. By Tarski's theorem, provability cannot align with truth, since then truth would be expressible. So there must be true unprovable statements.
Tarski's theorem admits proof similar to the fixed-point proof of Gödel's theorem, namely, if truth were expressible by T(x), then we could find a fixed point of nontruth λ⇔¬T('λ'), the Liar sentence λ, which asserts its own untruth, directly contradicting Tarski's requirement.
But Tarski's theorem also admits direct proof via Russell. Namely, if truth were expressible, then we could express R(x), asserting that if x is the code of φ, then φ(x̲) is not true, where x̲=1+⋯+1 is the numeral for x. If r='R(x)', then R(r) iff ¬R(r), a contradiction.
This is a direct proof of Tarski's theorem via Russell, bypassing Gödel. Reflection reveals that this is ultimately similar to the Gödel fixed-point proof, I would argue that this argument is simpler than the fixed-point lemma, which is itself derived from Russell.
In this way, Tarski's theorem is easier to prove than Gödel's, in that it requires less work in arithmetization and is also closer to Russell's elementary argument. The main point: we can prove Tarski's theorem straight from Russell, plus Gödel codes for assertions.
Furthermore, Tarski's theorem is stronger than Gödel's, since Gödel rules out only computably axiomatizable theories, but Tarski shows that no arithmetically definable theory captures truth, a far stronger result.
Conclusion: Gödel showed that truth does not align with provability in a given computable system. Tarski showed that truth is not arithmetically expressible, a stronger result, which is also easier to prove.
I wish I had made this point more strongly in my book. Chapter 7 is all about Gödel's theorem and Tarski's theorem and the connection with the Hilbert program, but I wasn't as forceful about this perspective when I wrote the book as I now feel is warranted. #PhilMaths
More succinctly: if truth were arithmetically expressible, then we could express the predicate R(x) asserting that x is an arithmetic formula that does not hold of its own Gödel code. If r is the Gödel code of R(x), then R(r) iff ¬R(r), a contradiction. Just like Russell.
• • •
Missing some Tweet in this thread? You can try to
force a refresh
