Non-standard Models of Arithmetic 17

Prev TOC Next

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 ∃xy(y=x)
AtMost2 iff ∃xyz(z=x z=y)
AtMost3 iff ∃xyzu(u=xu=yu=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”, ∀kn(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!

Prev TOC Next

Leave a comment

Filed under Conversations, Peano arithmetic

Non-standard Models of Arithmetic 16

Prev TOC Next

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

(x=\ulcorner\neg\alpha\urcorner\rightarrow\neg\text{True}_d(\ulcorner\alpha\urcorner))\wedge
\ldots\wedge(x=\ulcorner\exists u\alpha(u)\urcorner\rightarrow\exists y \text{True}_d(\ulcorner\alpha(y)\urcorner))

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

(d,n)\mapsto\ulcorner\text{True}_d(n)\urcorner

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 Σnn 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”: ∀xy[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.

Prev TOC Next

Leave a comment

Filed under Conversations, Peano arithmetic

Non-standard Models of Arithmetic 15

Prev TOC Next

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.

Continue reading

Leave a comment

Filed under Conversations, Peano arithmetic

Algebraic Geometry Jottings 18

Prev TOC Next

Up till now, I’ve been using power series to parametrize branches:

x(t) = a0+a1t+a2t2+ ⋯,      y(t) = b0+b1t+b2t2+ ⋯

If the branch passes through the origin, then a0=b0=0. In the last post, we established Facts 4 and 5, assuming that y(t)=t for all branches, so x(t) = a0+a1y+a2y2+ ⋯.

Continue reading

Leave a comment

Filed under Algebraic Geometry

Algebraic Geometry Jottings 17

Prev TOC Next

At last we come to Kendig’s proof of Bézout’s Theorem. Although not long, it will take me a few posts to appreciate it in full.

Continue reading

Leave a comment

Filed under Algebraic Geometry

Algebraic Geometry Jottings 16

Prev TOC Next

The Resultant, Episode 5: Inside the Episode

The double-product form for the resultant:

\text{res}_x(E,F) = a_m^n(y) b_n^m(y) \prod_{i=1}^m\prod_{j=1}^n (u_i-v_j)  (1)

implies Fact 3:

Continue reading

Leave a comment

Filed under Algebraic Geometry

Algebraic Geometry Jottings 15

Prev TOC Next

The Resultant, Episode 5 (The Finale)

Recap: The setting is an integral domain R, with fraction field K, and extension field L of K in which E(x) and F(x) split completely. E(x) and F(x) have coefficients in R. E(x) has degree m, F(x) degree n; we assume m,n>0. The main special case for us: R=k[y], K=k(y), so R[x]=k[x,y], and E and F are polynomials in x and y. As always, we assume k is algebraically closed.

Continue reading

Leave a comment

Filed under Algebraic Geometry

Algebraic Geometry Jottings 14

Prev TOC Next

The Resultant, Episode 4

This episode has one sole purpose: to show that the two formulas for the resultant are equivalent. The next episode, the finale, will tie up some loose ends.

Continue reading

Leave a comment

Filed under Algebraic Geometry

Weierstrass’s Smackdown of Dirichlet’s Principle

In 1856 Dirichlet made the following claim in a lecture:

Continue reading

Leave a comment

Filed under Analysis, History

The Monoenergetic Heresy (Part 1)

The Emperor Heraclius.
Classical Numismatic Group, Inc. Wikimedia Commons

And now for something completely different.

Continue reading

Leave a comment

Filed under Bagatelles, History