MW: To my mind, the heart of Enayat’s paper is Proposition 6 and Theorem 7, which combine to give Corollary 8.
Proposition 6: Every ZF-standard model of PA that is nonstandard is recursively saturated.
Theorem 7: Every countable recursively saturated model of PA+ΦT is a T-standard model of PA.
Corollary 8: The following statements are equivalent for a countable nonstandard model A of arithmetic:
- A is a T-standard model of PA.
- A is a recursively saturated model of PA+ΦT.
JB: Great! We’re getting to the heart of things now. There are some terms here that we discussed long ago, that the reader may have forgotten by now.
MW: Ok! I guess we should start with “recursively saturated”. That’s a model that realizes all recursive types. Which means we should review “types”. Actually, there’s a bit more to say about types, beyond what we said in posts 1, 2, and 9.
Let’s start with types in general, where we have a model M of some theory T (not necessarily set theory or arithmetic). The complete type of an n-tuple (or for short) is the set of all formulas such that . It’s the complete description of , or at least as complete as we make it in the language of T, L(T).
Also we have partial types: subsets of complete types. For example, we might consider all the existential formulas satisfied by , or all the formulas. We encountered partial types in the proof of the Paris-Harrington theorem.
But now let’s shift our perspective. Instead of types as descriptions, let’s look at them as wishlists. That is, consider a set p of formulas . The type p gives the properties we want the tuple to have. If there is such a tuple in M, then the type p is realized in M; otherwise, it’s omitted.
Wishlists are ok, but not fantasies: we insist that p be consistent with T. So, formally, we define an n-type of the theory T to be any set of formulas in L(T) that is consistent with T. Of course, here is an n-tuple of variables.
JB: Right, these are nice ideas! I think they’ll be very interesting to think about using categorical logic, since taking the complete type of an n-tuple of elements of a model is a way of extracting syntax from semantics, and the categorical approach aims for a kind of unification of syntax and semantics. But please carry on!
MW: Interesting point to bring up. You’ll notice that in switching from descriptions to wishlists, the model M has left the building. But we can sneak it back in through the back door by letting T be Th(M), the complete theory of M. Usually we do the name trick, where we throw in constants for every element of M; then we also call Th(M) the elementary diagram of M. The elementary diagram includes the atomic diagram (or just diagram), all the quantifier-free sentences true in M, but (again) with names for all the elements. Any model of the diagram of M includes an isomorphic copy of M. And the models of Th(M) are just the elementary extensions of M.
JB: Okay, cool. But the forgetful reader (who—don’t tell anyone—is secretly me) may be getting a bit drowned by detail. Maybe we’ll need all this soon. But the forgetful reader is waiting for you to remind them what a recursively saturated model is. So I should focus our conversation on that. Let me see if I’ve got you so far. You said it’s a model that realizes all recursive types. You’ve said what a type is: it’s a set of formulas in n free variables that can all be satisfied in some model of the given theory T. (More precisely this is an ‘n-type’.) If they’re all satisfied in the model M, we say the type is ‘realized’ in that model.
If this is right so far, you just need to remind me what a ‘recursive’ type is. I can guess: since a type is a set of sentences, we can demand that this set be recursive.
MW: That’s right. One more thing—a technicality, sort of, but important anyway—parameters. We’re allowed a bunch of names, say , appearing in the formulas making up the type. These parameters refer to elements of the model M.
So: We have a type p, or let me write it , to emphasize the variables and parameters. It’s a set of formulas . It’s satisfiable, meaning that in some elementary extension of M, we can make “all our wishes come true”: in this extension, the type is realized. And it’s recursive, when coded up as a set of Gödel numbers. ‘Recursive’ has a slightly tricky meaning here, because of the parameters, but we can get into that later.
Then M is recursively saturated if every such recursive type p is realized in M.
JB: Okay, I get it. So for the poor forgetful reader to understand the meaning of all the phrases in Enayat’s results at the top of this article, we just need to remind them of two things:
• What’s a ‘ZF-standard’ and more generally an ‘T-standard model’ of PA?
• What’s PA+ΦT? Here ΦT is the part that may need some explanation.
I’ll do the first part, since that’s all we need to understand Enayat’s Proposition 6. We started talking about ZF-standard models in Part 4, and reached T-standard models in Part 7. Let me quickly recap.
Enayat uses T to stand for some recursively axiomatizable extension of ZF (for example ZF itself). Inside any model of T there is a set called ω, the first infinite ordinal (according to the model). Taking this as our notion of natural numbers we get a model of PA. This is called a T-standard model of PA. Let me know if you want to improve this summary!
So, our poor addled reader has no excuse anymore for not understanding this:
Proposition 6: Every ZF-standard model of PA that is nonstandard is recursively saturated.
Or wait a minute. Maybe they do. What’s a nonstandard ZF-standard model of PA? I forget, we need to define that too! It sounds paradoxical.
MW: Indeed. It might help to change notation a tad. Let’s say U is our model of ZF. This isn’t the “true” universe of all sets (if there is such a beast), with the actual (“true”) element-of relation ∈. Instead, it’s a set U with a binary relation I’ll denote by ε, such that (U,ε) satisfies all the axioms of ZF. Note that U is a set. If we ever need a symbol for the “true” universe, we’ll use V.
If ε actually is ∈, then (U,ε) is a so-called standard model of ZF. Side note: A famous axiom, SM, says that there exists a standard model of ZF. SM can’t be proven from ZF, or even from ZFC+Con(ZFC).
Denote the “omega” of (U,ε) by ωU. And for the very forgetful reader, this is the set of all the finite ordinals, something we can define in ZF. Also ZF can prove that ωU is the first infinite ordinal, and can define + and · on ωU so that (ωU,+,·,0,1) satisfies all the axioms of PA. If (U,ε) is standard, then this just ℕ, the standard model of PA. But if (U,ε) is a nonstandard model of ZF, then ωU could be a nonstandard model of PA.
(Digression: it seems a bit unfair to write ωU for a nonstandard omega—after all, ε is responsible for any nonstandardness! Shouldn’t we write ω(U,ε)? But synecdoche says we should just write U to mean (U,ε).)
OK, so much for the nonstandard ZF-standard models. If you think ‘ZF-standard’ is a poor designation here, given the long-standing meaning of “standard model of ZF”, don’t blame me. I’d rather call them ‘omegas’.
JB: Wait, wait! Just let me see if I now understand what’s a ‘nonstandard ZF-standard model of PA’.
You’ve described the difference between ‘standard’ models of ZF (of which there could be many) and ‘nonstandard’ ones. Fixing any model of ZF, say (U,ε), we get a model of PA which you’re calling ωU—or ω(U,ε) if you’re in a pedantic mood. Any such model is, by definition, a ZF-standard model of PA.
But then there’s some other concept of a nonstandard model of PA, which I don’t think you explained just now. I guess it’s any model whose natural numbers aren’t equal to—or isomorphic to???—the model ωU for (U,ε) a standard model of ZF. Right?
MW: Exactly. It’s easiest to understand this from a Platonic perspective, aka naive set theory. There’s the standard model of PA, whose domain is order-isomorphic to the “true” ω. Up to isomorphism, there’s only one standard model of PA. All other models of PA are nonstandard. (I hasten to add that this perspective is a stylistic choice. It just means that we pretend there is an “outermost” universe containing everything we want to discuss, including U, but often other stuff outside U. What does this outermost universe look like? We don’t care, so long as it obeys the ZFC axioms. Which means the Platonic perspective is (or could be) just a way of talking about what can be proved from ZFC, but in T-shirt, shorts, and flip-flops, rather than black-tie.)
Any nonstandard model of PA contains a nonstandard element n, and hence an infinite descending sequence n > n–1 > n–2 > … That can’t happen in a standard model (U,∈). This is because ∈ is the same as < for ordinals, and the Foundation Axiom of ZF forbids an infinite descending ∈-chain of elements. So the ωU of any standard model (U,∈) of ZF is a standard model of PA.
As for ΦT , Enayat’s Theorem 4 states its key property: PA+ΦT is a recursive axiomatization of PAT. Recall that PAT is the set of sentences that hold in all ωU’s, as (U,ε) ranges over all models of T. Posts 13 and 14 went through the details of Theorem 4. We can chat about this more in the next post.