The Truth about Truth
MW: A little while back, I noted something delicious about the history of mathematical logic:
- Gödel’s two most famous results are the completeness theorem and the incompleteness theorem.
- Tarski’s two most famous results are the undefinability of truth and the definition of truth.
The Gödel fact is a bit of a cheat: ‘incomplete’ means something very different from ‘not complete’ in these two theorems. We don’t have that escape hatch with Tarski. Of course, ‘truth’ doesn’t have exactly the same meaning, or we’d have a genuine contradiction. But the two truths belong to the same concept web. The notions play as central a role in model theory (and math logic more broadly) as adjoint functors in category theory, so sorting out the fine points is worth a post or three.
By the way, logicians often talk about Satisfaction rather than Truth. It appears that Tarski anticipated one of Mick Jagger’s most famous songs.
Now, Tarski answered Pilate’s question with a very innocent-looking induction:
| True(φ ∧ ψ) | if and only if | True(φ) and True(ψ) |
| True(¬φ) | if and only if | not True(φ) |
| True(∃x φ(x)) | if and only if | there exists a c such that True(φ(c)) |
Truth for atomic sentences depends on the structure in question. For Peano arithmetic, this means defining the value of terms by an obvious induction, and then saying
| True(s=t) | if and only if | val(s) equals val(t) |
| True(s<t) | if and only if | val(s) is less than val(t) |
(If ‘<‘ is defined instead of a primitive symbol, then you don’t need the last clause.)
Of course, the right hand sides are all informal. But obviously we ought to be able to formalize Tarski’s definition, or else our formalizing apparatus (whatever it is) ain’t worth beans!
Sure enough, we can formalize the semantics of PA inside ZF. Painfully tedious, but with a magic wave of the hands, consider it done.
JB: Okay….
Wait a second! I’m a bit confused about this rule:
True(∃x φ(x)) if and only if there exists a c such that True(φ(c)).
What sort of c is this? A constant? That would be too restrictive. A term? Even that seems too restrictive! Wouldn’t it mean that ∃x φ(x) counts as true iff there’s something we can name that obeys φ? What about things like uncomputable numbers, or numbers that aren’t definable?
Oh, you’re just talking about PA now. So okay: people think all natural numbers should be nameable as 0, S0, SS0, SSS0, … Is that the point? So this is sort of special to PA?
MW: Good question! People handle this in a couple of superficially different ways. Or actually two and a half ways—the half being what you described. As you noted, this works only in special cases. Let’s scope out the general scene. We have a first-order theory A, in a language L(A), and a structure S for L(A). (I’ll use S both for the structure and the domain of the structure. I hope that doesn’t set your teeth on edge.)
Now, if there’s a term in L(A) for every element of S (as is the case with PA), then we can just say, c is a term.
For a general solution, we can expand the language L(A) by conjuring up a new constant for every element of S. Most people (me included) like to call these new constants names. So c is a name, with this approach.
Of course, the expanded language can now be uncountable! Model theorists have long since become blasé about this.
Still, some authors like a different approach. They define satisfaction not for a closed formula φ, but for a pair consisting of an arbitrary formula φ(x1,…,xn) and a value assignment assigning elements (c1,…,cn) of the structure to the free variables in the formula. The c’s are just elements of S, not part of the language L(A). They don’t expand the language. They’ll write S⊧φ[c1,…,cn] to mean that φ(x1,…,xn) is satisfied in S with the given value assignment. So, φ[c1,…,cn] isn’t really a formula at all for these people. It’s pretty clear though that the two approaches differ only in their flavor notes.
JB: Okay. I don’t mind focusing on the case of PA for now, since we’re talking about nonstandard models of arithmetic. So I guess you’re saying we can use this game to define a truth predicate in ZF, which I guess is really a predicate of natural numbers, such that True(n) means the sentence in PA with Gödel number n is ‘true’.
MW: That’s right. True for the structure ℕ. Since we’re working in ZF, we have other options for the argument of True. We can represent formulas as sequences of symbols, or parse trees. But these are minor details.
ZF isn’t the only game in town. Peano players have formalized truth using something called satisfaction classes (see Kaye, Chapter 15). We’ve talked about how doing the induction “on the outside” coughs up a whole series of truth formulas in PA, Trued. And there are other variations on this theme.
The real head-scratcher, it seems, is Tarki’s undefinability theorem. How come we can’t formalize True(φ) for PA inside PA? Or to state Tarski’s theorem more precisely: there no formula True(x) in the language of PA with one free variable, such that
where ⌜φ⌝ is the Gödel number of the sentence (closed formula) φ. Why not? That’s what we want to explore.
JB: That sounded a bit like the royal “we”, or actually its friend the authorial “we”, but yes—I too want to explore this. If PA is so good at talking about itself, why can’t it take Tarski’s definition of truth and somehow talk about that?
MW: I like that way of putting it. PA is self-aware in some ways, but not in others—just like people!
Tarski’s undefinability theorem is a direct transcription of the Liar Paradox: if we had a predicate ‘True(x)’, then we could construct a sentence saying “I am not true”. The self-referential aspect—the sentence talking about itself—that’s handled by Gödel’s diagonalization lemma. That topic could easily gobble up this whole post. We don’t want that, so I’ll dispose of it with two remarks. First, it has a genetic relation to Cantor’s diagonal argument (patron saint of this blog). Second, I find von Neumann’s theory of self-reproducing automata the most intuitive entry point to this topic: see §9.2 (pp.62–66) of my logic notes.
Anyway, let’s take the diagonality of Tarski’s theorem as a given. Here’s an analogy for why we can define Trued(x) formally, but not True(x). An imperfect analogy, to be sure—but if it wasn’t imperfect, it wouldn’t be an analogy! Let’s start to apply Cantor’s diagonal argument to an enumeration of, say, all rational numbers between 0 and 1. Thus:
0.50000…
0.33333…
0.25000…
0.66666…
0.20000…
If we break off after the first five entries, and do the usual “add 1” trick, we get 0.64171. Let’s say we pad it out with zeros. Sure enough, the rational number 0.641710000… doesn’t appear in the first five entries, but of course it does appear later on!
In the same way, we can construct a formula Trued(x) in L(PA) defining truth for all formulas of “complexity” at most d. So we can construct a formula that says, basically, “I am not trued”. But that formula has complexity greater than d.
Side note: I’m using parse tree depth as a measure of complexity. Some authors use the cruder notion of length. Of course, right-thinking folk regard formulas as parse trees and not just strings of symbols. On the other hand, in logic, Quantification is King. So logicians actually talk about SatΣn, satisfaction for Σn formulas (and likewise SatΠn). We may need to delve into that eventually.
Diagonal Argument 