MW: I’d like to chew a bit more on this matter of Trued 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:
AtMost1 iff ∃x∀y(y=x)
AtMost2 iff ∃x∃y∀z(z=x ∨ z=y)
AtMost3 iff ∃x∃y∃z∀u(u=x ∨ u=y ∨ u=z)
etc.
and then “exactly n elements” is easy:
Exactly1 iff AtMost1 ∧ ∃x(x=x)
Exactly2 iff AtMost2 ∧ ¬ AtMost1
Exactly3 iff AtMost3 ∧ ¬ AtMost2
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 Trued 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 Trued‘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, 10100 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, “Trued”. Then all of a sudden, out of the blue it seemed to me, you introduced something called SatΣn:
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.
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 Trued 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. Trued 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 Trued is defined.
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 Trued‘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 Trued 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, Trued 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 ⊢ Trued(⌜φ⌝) ↔ φ
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 Trued(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; Trued(⌜φ⌝) results from replacing n with the numeral for the Gödel number of the specific φ being considered. There’s a clause in Trued(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 Trued(⌜φ⌝) sentence down to the “val(x)=val(y)” clause and prove Trued(⌜φ⌝); if unequal, PA can likewise prove ¬Trued(⌜φ⌝). For the full nitty-gritty experience, note that PA has to use numerals for the Gödel numbers of the terms, and “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 Trued(n) handle negations and conjunctions, but quantification is the biggie. If φ is ∃xψ(x), then PA can parse ⌜φ⌝, and prove the equivalence of Trued(⌜φ⌝) to ∃xTrued-1(⌜ψ(x)⌝), basically because Trued-1 is copied into Trued in just this way. Some serious parsing going on: unlike with closed atomic formulas, we don’t eliminate the variables completely. The function k↦ ⌜ψ(k)⌝ is representable in PA (being recursive), so ∃xTrued-1(⌜ψ(x)⌝) say that there exists an x such that if y= ⌜ψ(x)⌝, then Trued-1(y). Unlike the case s=t, PA doesn’t determine the truth value of Trued(⌜∃xψ(x)⌝), just shows that it is equivalent to ∃xTrued-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 Trued(⌜φ⌝) ↔ φ 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 Trued before this!
Diagonal Argument 
I’ve just read parts 1-17, getting from each one to the next by clicking Next. But this one’s Next links (top and bottom) are black text, not links! Even though there is a next one, part 18 (probably just published).
(BTW is it too late to post comments to early parts (parts 4 or 5 or so) and expect replies?)
Link fixed, thanks! And please comment on any post on the blog.