MW: Ok, let’s plunge into the construction of Trued(x). The bedrock level: True0(x), truth for (closed) atomic formulas. For example, ‘s=t’ where s and t are terms. True0(x) isn’t just expressible in L(PA), it’s recursive. That is, let f(n) be the function which is 1 when n is the Gödel number of a closed formula s=t with s and t evaluating to the same number, and 0 otherwise. Then f is a recursive (i.e., computable) function. (That’s the sort of thing compilers do in their sleep.) And it’s a fact that all recursive functions are expressible in L(PA). See Kaye Chapter 3 for the hairy details, but this fact (I hope) evokes the response, “Sure, I’ll believe that.”
Now for the induction step. I outlined this in post 13: if we already have a formula Trued(x), then Trued+1(x) is the formula
where—and I can’t emphasize this enough—the occurrences of Trued are copied out in full, with the x’s being replaced with the arguments.
Let’s take a moment to consider that second line. A lot of mess hides behind the corner brackets. In prose, the line reads something like:
If x is the Gödel number of an existential sentence of the form ∃u α(u), then for some y, the Gödel number of the sentence obtained by substituting the numeral for y into α(u) satisfies Trued.
Mental checks to make sure this is kosher: is there a recursive function to see if x has the desired form, and to determine the Gödel number of the part α(u)? If we have the Gödel number for α(u) and a number y, is there a recursive function to find the Gödel number of the sentence obtained by substituting the numeral for y into α(u)? Check, check, and check, that’s all pure syntax. As for the quantification ∃y, that’s just an ordinary existential quantification in L(PA). (Unlike the ‘∃u’, which is inside the corner brackets.) Since all recursive functions can be represented in PA, we’re golden.
So the formulas Trued(x) get long, fast! But their Gödel numbers are still recursive. That is, the function
is a recursive function of d and n.
But this doesn’t help us construct the forbidden True(x)! After all, how would that work? The hypothetical True(x) would determine the parse tree depth d of the formula represented by x, then compute the Gödel number ⌜Trued(x)⌝ , and assert that this is the Gödel number of a true sentence. A vicious circle.
Especially important to note: quantifiers hidden inside Gödel numbers “bleed through” to explicit quantifiers in Trued+1. That was the point of contrasting ‘∃u’ inside the corner brackets with ∃y outside them.
Even worse: if you have something of the form ∃u ∀v α(u,v), which (recall) is an abbreviation for ∃u¬∃v¬α(u,v), then the negations also bleed through; at the end of the day, you have an explicit alternation of quantifiers ∃y ∀z. The upshot: if you rewrite Trued in prenex normal form, more and more alternating quantifiers pile up in front as d gets bigger and bigger. Kaye has the precise statement: SatΣn is a Σn formula, but not a Σn–1 formula.
JB: Okay! This is pretty nitty-gritty, but it took this amount of nittiness, and grittiness, for me to see how the quantifiers “bleed through” in the definition of Trued+1, making it have one more layer of quantifiers than Trued. It’s still amazing to me that no feat of encoding can manage to lump together all these Trued predicates and define the one true ‘True’ in PA. But I’m beginning to see it—and I do, after all, believe the proof of Tarski’s theorem.
MW: Yeah. I think asking why ‘True’ is undefinable in PA, is a bit like asking why the real numbers are uncountable. For any particular list of real numbers, we can find a number not on the list. But one might harbor the sneaking suspicion that if we were just a bit more clever, maybe we could find a work-around! Likewise, for any particular predicate T(x) claiming to formalize Truth for ℕ, we can find (using the diagonal lemma) a sentence φ for which it fails. But the feeling persists that there ought to be a way around this.
For you and me and readers of this blog, if we ever had these feelings about the uncountability of ℝ, they lie so long in the past that we don’t remember them. Poke around the internet, though, and you’ll find plenty of folks who still don’t believe Cantor’s diagonal argument.
JB: What’s SatΣn, exactly? The set of Gödel numbers of Σn sentences in the language of arithmetic that hold in, umm, the much-beloved “standard model” of PA? That would be okay with me: I assume we’re doing all our reasoning about this stuff either informally, or in some ambient set theory where we can define this standard model and prove its uniqueness.
MW: If you really want to see the nitty with the gritty, take a look at Kaye’s Chapter 9, “Satisfaction”. He begins it, “This is the chapter that no one wanted to have to write…”. Twenty-four pages of technicalities, climaxing in a formula that takes up almost an entire page!
‘Sat’ stands for ‘satisfaction’. Broadly speaking, SatΣn is much like Trued, a formula of L(PA) “defining truth” for a restricted class of sentences. Let’s go through the differences, mostly technical. First, you’ll recall the Σn/Πn hierarchy: the base level consists of the Δ0 formulas, where you’re allowed as much bounded quantification as you like, plus the logical connectives. For example, the definition of prime: Prime(x) iff x>1 ∧ (∀y<x)(∀z<x)[y>1 ∧ z>1 → ¬yz=x].
Then you stick alternating blocks of (unbounded) quantifiers in front. If you start with ∃, n blocks gives you a Σn formula; starting with ∀ gives a Πn formula. For example, the Π2 sentence “there are infinitely many primes”: ∀x∃y[y>x ∧ Prime(y)].
Next, you’ll recall that matter you brought up in the last post, about names for elements. SatΣn handles this by having two arguments, the first the Gödel number of a formula, the second the Gödel number of a finite sequence of arguments. So the intended meaning of SatΣn(x,y) is:
x is the Gödel number of a Σn formula φ(v1,…,vm), and y is the Gödel number of a sequence (c1,…,cm), and φ(c1,…,cm) is true.
That’s both nitty and gritty. But your question brings up a deeper and more important issue. True where? Why, in our working model of PA, whatever that is! That’s the intention, at least.
How can we formalize this intention? It looks like another vicious circle, where we’d need another definition of truth to justify this definition of truth. But in this case we’re lucky: we can strengthen “true” to “provable in PA”. We have, for any Σn formula φ(v1,…,vm),
PA ⊢ ∀y1…∀ym[SatΣn( ⌜φ(v1,…,vm)⌝ , ⌜(y1,…,ym)⌝ ) ↔ φ(y1,…,ym)]
Just a few things to note: first, we have a different proof for every such formula φ(v1,…,vm). Of course, all the proofs follow the same pattern. Second, the variables v1,…,vm occur inside the “Gödel number” corner brackets, while the y1,…,ym are outside. Finally, ⌜(y1,…,ym)⌝ stands for a recursive function coding finite sequences of numbers.
So if our working model is nonstandard, this all still makes sense!
We can say something similar for Trued. For any sentence φ of parse-tree depth at most d,
PA ⊢ Trued( ⌜φ⌝ ) ↔ φ
This is simpler, but not quite as good, since we don’t get to quantify over the arguments. If we turned Trued into a two-argument predicate, like SatΣn, then we’d have something pretty much the same.
Diagonal Argument 
Pingback: Recursive Saturation | Azimuth