**MW:** I’d like to chew a bit more on this matter of True* _{d}* versus True. This Janus-feature of the Tarski legacy fascinated me from the start, though I didn’t find it paradoxical. But now I’m getting an inkling of how it seems to you.

I thought of another analogy for the disconnect. Let’s look at the simplest first-order theory of them all, the theory of equality. You can formalize “there are at most *n* elements” for any *n* readily enough:

AtMost

_{1}iff ∃x∀y(y=x)

AtMost_{2}iff ∃x∃y∀z(z=x∨z=y)

AtMost_{3}iff ∃x∃y∃z∀u(u=x∨u=y∨u=z)

etc.

and then “exactly *n* elements” is easy:

Exactly

_{1}iff AtMost_{1}∧ ∃x(x=x)

Exactly_{2}iff AtMost_{2}∧ ¬ AtMost_{1}

Exactly_{3}iff AtMost_{3}∧ ¬ AtMost_{2}

etc.

but “there are only finitely many elements” can’t be expressed, by the compactness theorem.

**JB:** Yes, this doesn’t surprise me at all. Maybe once it would have, but it doesn’t now! But for some reason our ability to define True* _{d}* but not the one true True still bothers me. I have to make it seem more intuitive.

**MW:**The only response I have for that is two-fold: first, the vicious circle argument I mentioned, and next, the brute fact of Tarski’s theorem. Maybe there’s another intuition, but I haven’t found it. Well, the pile-up of alternating quantifiers in the True* _{d}*‘s is suggestive. We’ve known that alternating quantifiers spell complexity ever since the days of the Borel hierarchy.

**JB:** Okay. I think I’d internalized the lesson of Tarski’s undefinability of truth as *don’t try to define truth, you fool!* So even the thought of trying to define truth for sentences with at most, say, 10^{100} quantifiers sets alarm bells ringing in my head. But maybe I took the wrong lesson from this theorem!

I’m still worried about other things, though. Last time you were talking about how we define truth for sentences with at most *d* quantifiers, “True* _{d}*”. Then all of a sudden, out of the blue it seemed to me, you introduced something called Sat

_{Σn:}

The upshot: if you rewrite True

in prenex normal form, more and more alternating quantifiers pile up in front as_{d}dgets bigger and bigger. Kaye has the precise statement: Sat_{Σn}is a Σformula, but not a Σ_{n}formula._{n–1}

Then I made the mistake of asking what Sat_{Σn} was, instead of what I should have asked, which is “why are you talking about this now?” It sounds like True* _{d}* is a false front, and when we really get serious we should talk about Sat

_{Σn}instead. But that can’t be right, can it? What’s going on?

Later you say Sat_{Σn} captures satisfaction “in our working model of PA” for some class of sentences. I’m not so worried about which class—I’m worried about what our “working model” is and how Sat_{Σn} is so smart that it knows what this is.

**MW:** Yeah, I probably shouldn’t have brought up Sat_{Σn}. True* _{d}* is easier to explain; Sat

_{Σn}is more technical, but used for serious work. However, for 99% of what we’re doing (maybe 100%!), the difference doesn’t matter. I mentioned it in case someone goes looking in the literature (like in Kaye) and wonders where True

*is defined.*

_{d}Well, now that I *have* mentioned it, I have to say a bit more. The basic idea: you can define Truth *for* PA internally *in* PA provided you stick to sentences bounded by some “complexity measure”. The most naive possible measure: length, i.e., number of symbols. The True* _{d}*‘s get closer to “what really matters”, because they regard sentences as parse trees and not just strings. I don’t have a logical justification for that “what really matters” judgement; it’s just something I feel in my bones.

Now, according to the True* _{d}* sequence (

*d*=1,2,…), a negation or conjunction ups the complexity measure by 1: depth(¬φ)=depth(φ)+1, depth(φ∧ψ)=max(depth(φ),depth(ψ))+1. Likewise quantification. Sat

_{Σn}says, “No, what really matters are quantifiers! Increase the complexity measure by 1 for those, but not for the logical connectives.” And actually not just the

*number*of quantifiers, but the number of

*quantifier alternations*. Compare “There is an odd perfect number”, ∃

*n*(Oddperfect(

*n*)), with “There are infinitely many prime pairs”, ∀

*k*∃

*n*(

*n*>

*k*∧Prime(

*n*)∧Prime(

*n*+2)). Don’t you know in your bones that the second statement is more “complex” than the first? That’s the nub of the matter, but the formal definition involves prenex normal form and some other stuff, so maybe we should postpone that discussion until we need it (if ever).

Your other point is less technical and more significant, so if you’re okay with my brush-off of Sat_{Σn}, I’ll try to explain things better…

**JB:** Great! Yes, I’m fine with the idea that we can use different complexity measures. If I ever get serious about this stuff I can learn why some are technically better than others. And I’ve done some stuff with Σ_{n} and Π_{n} sets in measure theory (the Borel hierarchry) and an analogous hierarchy in recursion theory (the lightface hierarchy). So that general idea seems fine with me.

The other issue is more of a big deal.

**MW:** Good, I agree. Well, True* _{d}* doesn’t need to worry about

*which*model is our working model, since the key fact holds for

*all*models of PA. In other words, it’s a theorem of PA—or rather, an

*infinite family of theorems*. I mentioned this last time: for any sentence φ of parse-tree depth at most

*d*,

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

The proofs are tedious but not conceptually difficult. (Feel free to bail from this paragraph at any time.) If φ is atomic, say *s=t* where *s* and *t* are terms without free variables, then PA can check to see if *s* really does equal *t*. Or to be boringly precise, PA can prove the sentence “*s=t*” when the value of *s* does equal the value of *t*, and can prove “¬*s=t*” when it doesn’t. (PA sports a pocket calculator.) Now, one of the clauses of True* _{d}*(

*n*) says that if

*n*represents an atomic sentence of the form “

*x=y*“, then it holds if and only if val(

*x*)=val(

*y*). Again I will spell out the details at painful (or at least uncomfortable) length. First,

*n*,

*x*and

*y*are all variables here; True

*(⌜φ⌝) results from replacing*

_{d}*n*with the numeral for the Gödel number of the specific φ being considered. There’s a clause in True

*(*

_{d}*n*)

*including*the phrase “val(

*x*)=val(

*y*)”, which gets activated (so to speak) for this atomic φ. PA can extract the Gödel numbers for the terms

*s*and

*t*inside “

*s*=

*t*” (PA can parse things). If their values are equal, PA can then unwind the whole True

*(⌜φ⌝) sentence down to the “val(*

_{d}*x*)=val(

*y*)” clause and prove True

*(⌜φ⌝); if unequal, PA can likewise prove ¬True*

_{d}*(⌜φ⌝). For the full nitty-gritty experience, note that PA has to use numerals for the Gödel numbers of the terms, and “*

_{d}*u*=val(

*v*)” is a definable predicate, provable/disprovable when plugging in numerals for

*u*and

*v*, with the value on the left and the Gödel number of the term on the right. In short, PA can carry out formally all the steps you’d take to check that “1+(1+1)=(1+1)+1” holds and “1+0=0” doesn’t.

Whew! And we’re not done. Other clauses in True* _{d}*(

*n*) handle negations and conjunctions, but quantification is the biggie. If φ is ∃xψ(x), then PA can parse ⌜φ⌝, and prove the equivalence of True

*(⌜φ⌝) to ∃*

_{d}*x*True

_{d-1}(⌜ψ(

*x*)⌝), basically because True

_{d-1}is

*copied*into True

*in just this way. Some serious parsing going on: unlike with closed atomic formulas, we don’t eliminate the variables completely. The function*

_{d}*k*↦ ⌜ψ(

*k*)⌝ is representable in PA (being recursive), so ∃

*x*True

_{d-1}(⌜ψ(

*x*)⌝) say that there exists an

*x*such that if

*y*= ⌜ψ(

*x*)⌝, then True

_{d-1}(

*y*). Unlike the case

*s=t*, PA doesn’t determine the truth value of True

*(⌜∃*

_{d}*xψ(x)*⌝), just shows that it is equivalent to ∃

*x*True

_{d-1}(⌜ψ(

*x*)⌝).

Now you know why Kaye wrote, “This is the chapter that no one wanted to have to write.” Normally logicians don’t think about these details, anymore than topologists think about epsilons and deltas when showing that Boy’s surface is homeomorphic to a cross-cap plus disk. Once you get used to it, you just say: PA can handle syntax and can do grade school calculations, so proving True* _{d}*(⌜φ⌝) ↔ φ for any specific φ of depth at most

*d*is right up its alley. Perhaps quantification merits a moment’s further thought.

**JB:** Okay, I’m improving my intuition about this now. I don’t know why I’d never heard about True* _{d}* before this!