**MW:** Ok, let’s plunge into the construction of True* _{d}*(

*x*). The bedrock level: True

_{0}(

*x*), truth for (closed) atomic formulas. For example, ‘

*s*=

*t*’ where

*s*and

*t*are terms. True

_{0}(

*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 True* _{d}*(

*x*), then True

_{d}_{+1}(

*x*) is the formula

where—and I can’t emphasize this enough—the occurrences of True* _{d}* 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

xis the Gödel number of an existential sentence of the form ∃u α(u), then for somey, the Gödel number of the sentence obtained by substituting the numeral foryintoα(u) satisfies True._{d}

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 True* _{d}*(

*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 ⌜True_{d}(*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 True_{d}_{+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 True* _{d}* 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 Σ

*formula, but not a Σ*

_{n}*formula.*

_{n–1}**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 True_{d}_{+1}, making it have one more layer of quantifiers than True* _{d}*. It’s still amazing to me that no feat of encoding can manage to lump together all these True

*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.*

_{d}**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 True* _{d}*, 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:

xis the Gödel number of a Σ_{n}formula φ(v_{1},…,v_{m}), andyis the Gödel number of a sequence (c_{1},…,c_{m}), and φ(c_{1},…,c_{m}) 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 φ(*v*_{1},…,*v*_{m}),

PA ⊢ ∀*y*_{1}…∀*y*_{m}[Sat_{Σn}( ⌜φ(*v*_{1},…,*v*_{m})⌝ , ⌜(*y*_{1},…,*y*_{m})⌝ ) ↔ φ(*y*_{1},…,*y*_{m})]

Just a few things to note: first, we have a *different* proof for every such formula φ(*v*_{1},…,*v*_{m}). Of course, all the proofs follow the same pattern. Second, the variables *v*_{1},…,*v*_{m} occur *inside* the “Gödel number” corner brackets, while the *y*_{1},…,*y*_{m} are *outside*. Finally, ⌜(*y*_{1},…,*y*_{m})⌝ 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 True* _{d}*. For any sentence φ of parse-tree depth at most

*d*,

PA ⊢ True* _{d}*( ⌜φ⌝ ) ↔ φ

This is simpler, but not quite as good, since we don’t get to quantify over the arguments. If we turned True* _{d}* into a two-argument predicate, like Sat

_{Σn}, then we’d have something pretty much the same.