**MW:** OK, let’s recap the setup: we have a three-decker ω* ^{U}*⊂

*U*⊂

*V*. So far as

*U*is concerned, ω

*is the “real, true omega”.*

^{U}*V*knows it isn’t. Enayat’s question: what properties must an omega have, for it to be the omega of a model of

*T*? Here

*T*is a recursively axiomatizable extension of ZF, and

*U*is a model of it.

Obviously if *T* proves some assertion about omega, then ω* ^{U}* must satisfy it. PA

*stands for the set of all such sentences of L(PA); Enayat showed that PA+Φ*

^{T}*has the same deductive strength. But satisfying PA+Φ*

_{T}*isn’t enough! Prop. 6 identifies another requirement, namely recursive saturation. Theorem 7 shows that for countable models of PA, this (together with PA+Φ*

_{T}*) is sufficient.*

_{T}The question presents itself: *why* isn’t PA+Φ* _{T}* all you need?

Let me start with some good old hand waving. PA+Φ* _{T}* captures all the requirements

*that can be expressed in the language of Peano arithmetic*. Think of the relation between

*U*and ω

*as between parent and child. The parent knows lots of things they can tell their child, things the child doesn’t know on her own. But at least the child can understand them. For other things, though, the parent trots out that famous and frustrating phrase, “You’ll understand what that means when you’re older.”*

^{U}So, ω* ^{U}* understands what Con(PA) means, even though PA can’t prove this. But ZF can. However, “ω

*is recursively saturated” can’t even be expressed in L(PA), but it can in L(ZF).*

^{U}But now for a subtle twist, that will delight you. *U* doesn’t think that ω* ^{U}* is recursively saturated.

*U*thinks that ω

*is “the standard omega”! Only*

^{U}*V*can see the recursive saturation of ω

*. (Maybe*

^{U}*V*is the grandparent?)

**JB:** I’m not sure it delights me yet. It certainly shocks me, though! And in math, shock comes before delight.

I can see why ω* ^{U}* could need some extra property that

*U*can’t see, for it to be standard in

*V*. That doesn’t shock me. What shocks me is the precise nature of this extra property: recursive saturation. This seems to say that ω

*is “big and fat”, containing all sorts of wild and crazy nonstandard numbers. Why should it be like that?*

^{U}**MW:** Good, let’s dig into that. First though, a useful perspective on types. We can think of them as *infinite conjunctions*. A type *p*(*x*) = {φ_{i}(*x*):*i*∈*I*}} amounts to the infinite formula ⋀_{i∈I} φ* _{i}*(

*x*). (In fact, type theory has close connections with the infinitary language known as L

_{∞ω}.) I’ll sometimes write types with this more suggestive notation.

Say *N* is the ω* ^{U}* of a model

*U*of ZF, and suppose

*N*is

*not*the standard ω. (As we’ve been discussing elsewhere,

*N*can be the standard ℕ, even if

*U*is not “the real universe

*V*”. In that case,

*N*won’t be recursively saturated, of course.)

Let’s start with an easy type, ⋀_{k∈ω} *x*>*k*. That “*k*∈ω” stands for all the *standard* integers, and “*k*” denotes the numeral for *k*. So this wishlist just asks for a *c* satisfying *c*>0, *c*>1, … *N* has such a *c* (“realizes the type”) because we’ve assumed *N* is nonstandard. But you also might say, *N* must have such a *c* by overspill.

**JB:** Let’s see if I can remember how that overspill argument goes. This is a weak version of the overspill lemma; there are stronger ones:

**Overspill Lemma.** In a nonstandard model of Peano arithmetic, any predicate in the language of arithmetic that holds for infinitely many standard natural numbers also holds for infinitely many nonstandard ones.

How can we use this to get the job done? Well, in this particular case *one* way is to use the predicate *P*(*n*) = ∃*x*(*x* > *n*). This holds for all standard *n*, so it holds for some nonstandard *n*, and we can use that to prove (at least out here, using all the math we know) that this *n* realizes the type ⋀_{k∈ω} *x*>*k*.

But somehow I fear this isn’t the method you intended. How would you use overspill here?

**MW:** OK. What you did works. But it used a special feature of this type. Namely, “*x*>*k*” implies “*x*>*l*” for any *l*<*k*. So that makes it harder to generalize.

**JB:** Right. That’s why I was suspicious of this approach: I couldn’t see how it generalizes. So how did you *intend* to use overspill here?

**MW:** Hmm, maybe the simple example was *too* simple. That happens sometimes; you need an example with some bite to it, to spark the right neurons.** ** How about this. We will show that *N* contains a number divisible by all standard primes. So let prime(*x*) stand for the *x*-th prime number. We can formalize this in L(PA). Now let’s consider the type

*p*(*x*) = ⋀_{k∈ω} prime(*k*)|*x*

For any finite *n*, the formula ∃*x*(⋀_{k≤n} prime(*k*)|*x*) holds in *N*: there’s always a number divisible by the first *n* primes. So by overspill, our type *p*(*x*) is realized in *N*.

As you pointed out, the trick is to choose the right predicate, call it *P*(*w*). We want *P*(*n*) to hold for all finite *n*; *P*(*c*), for nonstandard *c*, should imply that some number is divisible by all standard primes. The predicate *P*(*w*) = ∃*x*(prime(*w*)|*x*) does *not* work—*P*(*c*) for nonstandard *c* tells us that some number is divisible by some nonstandard prime. Not what we’re aiming for. So what predicate *do* we want?

If you look over the last three paragraphs, one answer should come to mind right away (I hope). Let’s start with that. You might see a problem with it, but ignore that for now. What’s the easy, maybe-not-quite-right answer?

**JB:** How about the predicate *P*(*n*) given by ∃*x*(∀*k* *k≤**n* → prime(*k*)|*x*)?

By the way, I always hate how logicians use symbols when words would do just as well, but now I’m doing it too. I’m suggesting a predicate *P*(*n*) that says there exists a number that’s divisible by the first *n* primes.

**MW:** I know what you mean. I made some remarks about this in my review of Smullyan & Fitting’s Set Theory and the Continuum Problem. On the other hand, sometimes I think the logical notation makes things clearer. Maybe Cauchy wouldn’t have flubbed uniform convergence the first time, if he’d had modern notation! (See my post on the Arithmetical Hierarchy.)

In this case, the notation is fully justified, since it’s intended as a short-hand for some formula in the formal language. It’s a fully formal formula, in casual clothes, so to speak. I call this sort of “formal-but-not-quite” language ‘vernacular’.

Anyway, yes, that’s the predicate I had in mind. Now comes the question, are we sure this *can* be translated into a formal predicate? We need either to convince ourselves the answer is yes, without actually writing out the formal translation, or else realize why not.

**JB:** So, it seems that if we’re trying to translate ∃*x*(∀*k* *k≤**n* → prime(*k*)|*x*) into a formal predicate in the language of PA, the two hard parts could be prime(*k*), the *k*th prime, and |, the divisibility relation. The divisibility relation is actually easy: *x*|*y* is just short for “there exists *a* such that *ax*=*y*”. The *k*th prime is a lot harder, but I seem to recall doing this and a lot of other things when I took logic with Kripke as an undergrad. He was a real taskmaster! He said he didn’t want to raise a generation of mathematicians who would take the Church–Turing thesis on faith. So he made us write piles of well-formed formulas to show that we could create a provability predicate for PA. I forget all the details, but I think back then I could have written a formal predicate for prime(*k*) in the language of PA… in principle. Of course we broke these problems down into parts.

**MW:** Kripke! Wow! Way to go!

Yes, that’s what I had in mind. Note the small but significant shift from a variable-length conjunction ⋀_{k∈ω} to a bounded quantifier ∀*k**≤**n*. (You wrote it out explicitly, “∀*k* *k≤**n* →”, but as we know already, bounded quantifiers play a fundamental role in Peano Arithmetic.)

Ready for the general case? A type *p*(*x*) = ⋀_{i∈I} φ* _{i}*(

*x*), where

*I*is a recursive subset of ω, and {φ

*(*

_{i}*x*) :

*i*∈ω} is a so-called effective listing of formulas with

*x*free? (I’m being a bit vague, since we will need to discuss parameters. Let me know if you want to address that upfront, or put it off just a little longer.)

**JB:** Let’s skip the parameters—I’m happy to accept things can be done in a parametrized way if I see how to do them at all. So, I think we can use the predicate ∃*x* ∀*k**≤**n* φ* _{f(k)}*(

*x*), where

*f*is a recursive function, defined in the language of PA, that enumerates your set

*I*. If we have a nonstandard model of PA for which this holds for all standard

*n*, it must also hold for some nonstandard

*n*, by overspill.

Is that where we’re heading? By the way, I only seemed to use the assumption that *I* is recursively enumerable.

**MW:** Right idea. But is it OK to replace the variable-length conjunction φ_{f(1)}(*x*)∧…∧φ_{f(n)}(*x*) with the bounded quantifier ∀*k**≤**n* φ* _{f(k)}*(

*x*)? How would you formalize that? We need a formal predicate

*P*(

*n*) in order to apply overspill.

The replacement of “recursive” with “recursively enumerable” *should* be a yellow flag, since the difference usually *is* a big deal. But remember Craig’s trick. You can use it show that “recursively saturated” and “r.e. saturated” are equivalent. (Kaye does this on p.150.) So no problem here.

**JB:** Cool! It’s gonna take me longer to get used to Craig’s trick.

I don’t get what’s wrong with ∀*k**≤**n* φ* _{f(k)}*(

*x*). I thought

*f*was some recursive function written out in the language of PA. So I thought this whole thing was… or could be expanded out to become… a perfectly kosher predicate

*P*(

*n*).

Are you trying to catch me in a technicality? Or is there some profound issue here? (I guess logic is a subject where the borderline between technicalities and profound issues is rather thin.)

**MW: **As for the thin borderline, I dunno. I remember you once wrote that learning category theory makes you grow new neurons. (Or should that be synapses?) True for me, certainly. But category theory has no monopoly on that!

Anyway yes, it’s pretty significant, maybe profound. *P*(*n*) needs to be a *single* formula in L(PA) with one free variable. But φ* _{f(k)}*(

*x*) is a

*different*formula for every value of

*k*. Put another way, the

*x*is a variable in good standing in L(PA), but

*k*is a meta-variable—a variable in the meta-language, which in this case is a hybrid of symbols and prose.

You are correct that the Gödel number of φ* _{f(k)}*(

*x*) is a recursive function of

*k*. Use that.

Another thing to ponder: so far, everything we’ve said holds for any nonstandard model of PA. But they’re not all recursively saturated!

**JB:** Okay, I was making a mental slip. I though that φ* _{f(k)}*(

*x*) was a single formula with two free variables

*k*and

*x*, one of which you were writing as a subscript just for kicks.

Now I don’t see how to do this problem.

Part of why I had such trouble with your end run around Tarski’s theorem on the undefinability of truth is that I couldn’t believe it was impossible to take an infinite disjunction like True_{1}(*x*)∨True_{2}(*x*)∨… and turn it into a formula in PA, given that the Gödel number of True_{d}(*x*) depends recursively on *d*. I was thinking it could be turned into some formula like ∃*d* *P*(*d*,*x*). But no. It was just an illusion that dissolved when I looked closely.

Now you’re getting me from the other direction. I don’t see how to use the fact that the Gödel number of φ* _{f(k)}*(

*x*) is a recursive function of

*k*to cook up a formula

*P*(

*n*) that “means” ∀

*k*

*≤*

*n*φ

*(*

_{f(k)}*x*).

**MW:** Yup, same circle of ideas. Indeed, if all we know is that *N* is a nonstandard model of PA, then there’s no way around it: *N* might *not* be recursively saturated.

Here’s another hint: let’s say a type ⋀_{k∈ω} φ_{f}_{(}_{k}_{)}(*x*) is a *d*-type if every φ_{f}_{(}_{k}_{)}(*x*) appearing in it has complexity (parse-depth) at most *d*. Let’s say *N* is recursively *d-*saturated if every recursive *d*-type is realized. So this is weaker than recursively saturated. Every nonstandard model of PA is recursively *d-*saturated. Do you see how to prove that?

**JB:** Okay, good! I think I do, but before I try let me straighten something out. It seems I need those ‘parameters’ you were threatening me with. Back in Part 15 and Part 16 you explained True_{d}, a predicate such that if φ is a sentence of complexity at most *d*, then PA can prove φ is equivalent to True_{d}(⌜φ⌝), where ⌜φ⌝ is the Gödel number of φ:

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

But in our conversation now we have this free variable *x* running around. To prove what you want, I seem to need a parametrized version of True_{d}, such that if φ(*x*) is a formula of complexity at most *d* containing one free variable *x* we have

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

*x*) ↔ φ(

*x*)

This is a mutant version of True* _{d}* that takes two arguments, not one. Am I on the right track, or am I confused again?

**MW:** Right on the money!

And now that parameters have reared their heads, maybe it’s time to cover them properly. First, True* _{d}* should undergo a further mutation, to allow an arbitrary number of free variables in φ, say . Then we’ll get

Here is the list of elements coded up as a single element. PA has a bunch of these coding schemes, even allowing for variable length lists; Gödel gave the first one in his famous incompleteness paper in 1931. (He used the Chinese Remainder Theorem.)

However, for our purposes, I think we can stick with your version.

Second, what is a ‘recursive type’ when you allow parameters? Just one parameter for now, say *a*, that’s enough to give the idea. We’d like the Gödel numbers of the formulas in ⋀_{i∈I} φ* _{i}*(

*x,a*) to be recursive. The notation does most of the work: say {φ

*(*

_{i}*x,u*):

*i*∈ω} is an effective enumeration of formulas of L(PA) with two free variables. Write

*p*(

*x*,

*u*) = ⋀

_{i∈I}φ

*(*

_{i}*x*,

*u*), with

*u*a free variable, and

*p*(

*x*,

*a*) = ⋀

_{i∈I}φ

*(*

_{i}*x*,

*a*), with

*a*an element of our model

*N*. Then

*p*(

*x*,

*a*) is a

*parametrized type*of

*N*, provided it’s

*finitely satisfied*in

*N*. It’s

*recursive*when

*I*is recursive.

*N*is

*recursively saturated*when all its recursive parametrized types are realized.

So that’s the trick: compute the Gödel numbers of the formulas* before* plugging in the value of the parameter.

Oh yes, you can represent the recursive set *I* as the range of a recursive function *f* if you like, as we’ve been doing.

**JB:** Oh, great! Then I think I know what to do. But before I do it, let me describe a simpler variant that doesn’t use this “parametrized True* _{d}*” stuff. Instead of a recursive family of one-variable predicates φ

*(*

_{f(k)}*x*), let’s suppose we have a two-variable predicate

*Q*(

*k*,

*x*).

Let

*P*(*n*) = ∃*x* ∀*k*≤*n* *Q*(*k*,*x*).

So *P*(*n*) is saying that we can find an *x* that makes a bunch of stuff true: *Q*(0,*x*), *Q*(1,*x*),…, on up to *Q*(*n*,*x*). Now, suppose PA can prove *P*(*n*) for each standard *n*. Then by overspill, in a nonstandard model we must also have *P*(*n*) for some nonstandard *n*. It seems this implies there’s an element *x* in our model that obeys *Q*(*k*,*x*) for all standard *k*.

This is some sort of “saturation” property of nonstandard models of PA that seems like a relative of recursive saturation… but simpler. Did I make a mistake somewhere? After you answer, I’ll go back and do what I was supposed to do. But this seems similar, and simpler. So I’m wondering why we went straight to the more complicated version.

**MW:** No mistake. Let’s call your version Q-saturation. You’ve just shown that any nonstandard model of PA is Q-saturated. My recursive *d-*saturation implies your Q-saturation, because *Q* has some complexity *d* which is inherited by all the instances *Q*(*k*,*x*). Conversely, Q-saturation implies recursive *d-*saturation. All you need is a formula *Q*(*y*,*x*) with two free variables such that

*Q*(*k*,*x*) ≡ φ* _{f(k)}*(

*x*).

The equivalence here means that one side holds in our model *N* iff the other side does, for any *x* and any standard *k*.

Equivalent to both Q and recursive *d*-saturation is recursive Σ* _{n}*-saturation, which is what Kaye and other professionals use.

Anyway, to repeat: any nonstandard model of PA has Q-saturation = recursive d-saturation = recursive Σ* _{n}*-saturation. So Enayat’s result shows that in exchange for the hypothesis of being ZF-standard, you get the stronger property of recursive saturation, not shared by all nonstandard PA models.

**JB:** Okay, I get it: my form of saturation is already studied, but it’s weaker than recursive saturation. Now I’ll finish doing the task you assigned me—it’s obvious to *you* what I’m up to, but some readers may want it spelled out, especially given all my digressions.

We’re trying to show any nonstandard model of PA is recursively *d*-saturated. So, suppose the predicate φ_{f}_{(}_{k}_{)}(*x*) has complexity at most *d* for all standard *k*. Fix a nonstandard model of PA, and suppose for every standard *n* there exists an element *x* of this model such that

φ_{f(1)}(*x*)∧…∧φ_{f(n)}(*x*).

Then we need to show there’s an element *x* of our nonstandard model obeying φ_{f}_{(}_{k}_{)}(*x*) for *all* standard *k*.

To get the job done, I’ll use my mutant True* _{d}* predicate with

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

*x*) ↔ φ(

*x*)

and define

*Q*(*k*,*x*) = True* _{d}*( ⌜φ

*⌝,*

_{f(k)}*x*)

This trick converts our indexed family of predicates into a single 2-variable predicate. That is, we have

PA ⊢ *Q*(*k*,*x*) ↔ φ* _{f(k)}*(

*x*)

Then we can use the overspill argument that I sketched earlier to show that in our nonstandard model of PA there exists *x* obeying *Q*(*k*,*x*) for all standard *k*. But this is the same as obeying φ* _{f(k)}*(

*x*) for all standard

*k*.

By the way, I’ve been wondering why you use the letter *d* in your predicate True* _{d}*. Do you have a cousin named Trudy?

**MW:** I use *d* for depth, and also to give *n* a rest—she deserves it! But I like your idea. From now on, I’ll think of my imaginary cousin Trudy every time a truth predicate comes up.

OK, good work! I think you’re ready for Enayat’s Prop. 6. I’ll just quote the statement and proof for you to chew on until the next post.

Proposition 6:Every ZF-standard model of PA that is nonstandard is recursively saturated.

Proof:ZF can define the Tarskian satisfaction predicate for every set structure; and in particular it can do so for ℕ. In light of this observation, recursive saturation follows from a routine overspill argument, as in Kaye, Proposition 15.4.

Kaye’s Prop. 15.4 says that every nonstandard model of PA is Σ* _{n}*-saturated for all

*n*. Guess he doesn’t have a cousin Trudy.

**JB:** Wow! Enayat proves a stronger result in 4 lines than I could prove after a whole page of conversation. I guess knowing what you’re doing really does help.

**MW:** Stronger hypothesis, stronger conclusion.

Pingback: Enayat on Nonstandard Numbers | Azimuth