**MW:** Enayat’s second major result is:

**Theorem 7:** Every countable recursively saturated model of PA+Φ* _{T}* is a

*T*-standard model of PA.

Recall the definition of Φ* _{T}*: the set of formulas of the form

{φ → Con(*T _{n}*+φ

^{ℕ}) : φ∈L(PA),

*n*∈ℕ}

where *T _{n}* is the first

*n*statements of

*T*, and φ

^{ℕ}is φ∈L(PA) translated into a formula of L(ZF).

Notice the countability condition, which was not needed for the reverse result, Proposition 6. Enayat mentions that the quickest way to prove the theorem is via a replendence argument. Someday I may do a post about this, but the proof he gives is worth our attention. It falls into four parts. Let *N* be a countable recursively saturated model of PA+Φ* _{T}*. Here’s a quick preview—details to come, so don’t worry if not all of it makes sense yet.

- Using the Arithmetized Completeness Theorem, plus recursive saturation, he obtains a model
*U*of*T*whose ω is both an end-extension of*N*and elementarily equivalent to it: ω⊇^{U}_{e}*N*and Th(ω)=Th(^{U}*N*). (Recall that Th(*N*) is the set of all sentences of L(PA) that hold in*N*, and likewise for Th(ω).)^{U} - Next he observes that Proposition 6 applies to ω
, so it’s recursively saturated.^{U} - Since ω
⊇^{U}_{e}*N*, their*standard systems*are the same: SSy(ω)=SSy(^{U}*N*). The standard system of a nonstandard model of PA is the family of subsets of ℕ that can be coded by elements of the model. - Finally, he notes that any two countable recursively saturated models of PA are isomorphic if they have the same first-order theory and the same standard system. That is, if Th(
*M*)=Th(*N*) and SSy(*M*)=SSy(*N*) and*M*and*N*are countable and recursively saturated, then*M*≅*N*. So*N*is isomorphic to the ω of a model of*T*. But that’s the definition of*T*-standard. QED

The rest of this post expands on (1), with (2)–(4) relegated to later posts. Let’s start with the Arithmetized Completeness Theorem (ACT). I wrote a Topics post about this, but it’s pretty long so I’ll just cherry-pick the info we need.

The Completeness Theorem says that a consistent theory *T* has a model *U*. The ACT says that a consistent arithmetic (aka representable) theory has an arithmetic model. *Arithmetic* here means definable via formulas of L(PA). Thus, the set of Gödel numbers of the axioms of *T* is definable by a formula of L(PA): φ∈*T* iff θ(⌜φ⌝) holds, for some θ(*x*)∈L(PA). Likewise, the domain, relations, constants, and functions of *U* are all specified by formulas in L(PA).

Moreover, the ACT says this can all be proved inside PA. The proof of the ACT shows how, starting with a formula defining a consistent *T*, we can whip up formulas for the all the semantic aspects of *U*. Foremost among these is the truth predicate Sat* _{U}*: Sat

*:(⌜φ⌝) for a sentence φ expresses the fact that*

_{U}*U*satisfies φ.

It’s convenient to gloss over the distinction between a formula and its Gödel number, so I’ll mostly omit the brackets ⌜⌝ below. Imagine that formulas *are* numbers.

Because all this is happening inside PA, we can apply it to any model *N*. For nonstandard *N*, matters take a curious turn. First off, we’ll have *nonstandard formulas*, including some of *nonstandard length*. (If Formula(*x*) is the formalization of “*x* is a formula”, then any nonstandard *d* satisfying Formula(*d*) represents a nonstandard formula.)

The truth predicate Sat* _{U}* defines satisfaction for all sentences in the language of

*T*, including nonstandard ones. The proof of the ACT shows that Sat

*extends ordinary standard satisfaction: if φ is standard, then Sat*

_{U}*(φ) iff*

_{U}*U*⊧φ. To avoid confusion, I will use the symbol ⊧ only for satisfaction in the standard sense.

The notion of consistency also demands a second look. Con(*T*), a sentence in the language of arithmetic, says that there is *no* proof of a contradiction, not just no *standard* proof. An instructive example: by Gödel’s Second Incompleteness Theorem, the theory PA+¬Con(PA) is consistent. Suppose *N* is a model of it. Then *N*⊧¬Con(PA). So in *N*, there is a proof of a contradiction, but no standard proof.

The ACT demands that *N*⊧Con(*T*) before it goes to work. Showing that *T* is consistent in the standard sense doesn’t cut it.

OK, let’s look at Enayat’s step (1). We need to construct a model of *T*, starting with a model of PA. Not only that, but Φ* _{T}* is knocking on the door of Con(

*T*). This suggests using the ACT. Larry Manevitz observed (in the 70s) something similar. Let

*N*be a model of PA. Then

If *N*⊧Con(ZF), then there is a model of ZF whose ω is an end extension of *N*.

If *N*⊧Con(ZF), the ACT immediately hands us a model *U* of ZF. Manevitz’s result falls out from looking at the recursion that imbeds ℕ as an initial segment of *any* model (say *M*) of PA. You recursively define a map *n*↦*n ^{M}* with Successor(

*n*)↦Successor

*(*

^{M}*n*). A straightforward induction shows that the image is an initial segment. This can all be formalized in PA, so it works for any model

^{M}*N*of PA. In particular,

*N*an be imbedded as an initial segment of ω

*. That’s Manevitz’s result. It works without change for any arithmetic extension*

^{U}*T*of ZF: if

*N*⊧Con(

*T*), then there is a model of

*T*whose ω is an end extension of

*N*.

We just need to deal with two issues to get Enayat’s step (1):

- Φ
gives us Con(_{T}*T*) for any_{n}*n*∈ℕ. (Just let φ ≡ 1=1.) This is not quite the same as Con(*T*). - We also need Th(ω
)=Th(^{U}*N*).

For the first bullet point, we *might* think we’re in the clear since Con(*T _{n}*) for all

*n*∈ℕ implies that

*T*is consistent. But we saw above that

*N*⊧Con(

*T*) is stronger. Overspill comes to the rescue. Since

*N*⊧Con(

*T*) for all

_{n}*n*∈ℕ, we have

*N*⊧Con(

*T*) for some nonstandard

_{d}*d*. We can apply the ACT to

*T*to get a model

_{d}*U*of it. But

*T*includes all the standard formulas of

_{d}*T*, so

*U*⊧

*T*with

*T*interpreted in the standard sense.

For the second bullet point, we appeal to recursive saturation. The trick here: code Th(*N*) via a nonstandard element of *N*. Any element *v* of *N* can be regarded as a bitstring; let’s write *v _{i}* for the

*i*-th bit of

*v*. Also write φ

*for the sentence with Gödel number*

_{i}*i*. If

*v*is to code Th(

*N*), we need

*v*=1 when

_{i}*N*⊧φ

*and*

_{i}*v*=0 when

_{i}*N*⊧¬φ

*. In other words,*

_{i}*N*⊧(φ* _{i}* ↔

*v*=1).

_{i}Now, the set {φ* _{i}* ↔

*v*=1 :

_{i}*i*∈ℕ} is a recursive set of formulas with the free variable

*v*. It is obviously finitely satisfiable, so it’s a recursive type. Recursive saturation says there is an element

*a*∈

*N*realizing this type:

*N*⊧(φ* _{i}*↔

*a*=1), for all

_{i}*i*∈ℕ.

Next step is to whip up a theory combining *T* and Th(*N*). Once again we do this first for finite fragments of the theory. Let

Γ(*n*) = *T _{n}*+{φ

_{i}^{ℕ}:

*i*<

*n*and

*a*=1}

_{i}*N*⊧Φ* _{T}* tells us that

*N*⊧Con(Γ(

*n*)) for all

*n*∈ℕ. By overspill,

*N*⊧Con(Γ(

*d*)) for some nonstandard

*d*. Apply the ACT to Γ(

*d*). It hands us a

*U*satisfying Γ(

*d*).

*A fortiori*

*U*is a model of

*T*(standardly speaking) and of exactly those φ

_{i}^{ℕ}that hold in

*N*. For the record, note that

*N*“believes” there are nonstandard sentences φ

_{e}^{ℕ}, but if

*e*>

*d*then Γ(

*d*) says nothing about them. Fortunately, we care about φ

_{i}^{ℕ}only for standard

*i*. Summing up, Th(ω

*)=Th(*

^{U}*N*), and by the Manevitz argument, ω

*⊇*

^{U}_{e}

*N*. (1) is done!

Finally, a point to ponder. It looks as though the ACT-provided truth predicate Sat* _{U}* offers a way around Tarski’s Undefinability Theorem. Namely,

*N*⊧φ iff Sat

*(φ*

_{U}^{ℕ}). What gives?

The answer lies buried in the details of Topics 4 (the Addendum) and Topics 10 (a remark at the end of the Proof Sketch). I’ll explain next time.