**MW:** We’re still going through Enayat’s proof of his Theorem 7:

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

*T*-standard model of PA.

We’ve already done step (1). We obtained 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*). Now it’s time for the next two steps:

- 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.

(2) is like falling off a log. Prop 6 says that if the omega of a model of ZF is nonstandard, then it’s recursively saturated. *U* is a model *T*, which extends ZF. *N* is nonstandard (it’s recursively saturated), and ω* ^{U}*⊇

_{e}

*N*, so ω

*is nonstandard. Kaboom! Done!*

^{U}I like that this step uses the *converse* of Theorem 7 to help prove Theorem 7. (Technically Prop. 6 is stronger than the converse to Theorem 7, because the countability condition is dropped.) I can’t think of another case where you use the converse of a theorem in proving the theorem.

Step (3) is not hard, but perhaps I should first clear away some preliminaries. What do we mean by coded? We have several options. I prefer using bitstrings: if (say) [*n*]* _{i}* stands for the

*i*-th bit of

*n*, regarded as a bitstring, then

*n*codes {

*i*: [

*n*]

*=1}. Kaye prefers to use the coding of arbitrary length sequences. He uses (*

_{i}*n*)

*to denote the*

_{i}*i*-th item in a sequence coded by

*n*, using the Gödel β-function coding. Then he says that

*n*codes {

*i*: (

*n*)

*≠0}. These details don’t matter: the key is that both [*

_{i}*n*]

*=1 and (*

_{i}*n*)

*≠0 are Δ*

_{i}_{1}formulas. (As it happens, they are even Δ

_{0}. Δ

_{1}is clear, since they’re both recursive, but Δ

_{0}is not at all obvious.) Another property, also shared by the two formulas, will be important. I’ll use my preferred bitstrings below.

Claim: if *M* and *N* are models of PA, and *M*⊆_{e}*N*, then SSy(*M*)=SSy(*N*). One direction is *really* easy. Say *m*∈*M* codes *S*={*i*∈ℕ : *M*⊧[*m*]* _{i}*=1}. Since

*M*⊆

_{e}

*N*we have

*M*≼

_{Δ1}

*N*(see Topics 8). Thus

*M*⊧[

*m*]

*=1 iff*

_{i}*N*⊧[

*m*]

*=1. So*

_{i}*m*codes the same subset of ℕ in both

*M*and

*N*, and so SSy(

*M*)⊆SSy(

*N*).

In the other direction, say *n*∈*N* codes *S=*{*i*∈ℕ : *N*⊧[*n*]* _{i}*=1}. We need to find an

*m*∈

*M*also coding

*S*. Now,

*n*represents a non-standard length bitstring, but we care only about the initial segment of “length” ℕ. All we need, then, is for

*m*and

*n*to agree as bitstrings up to some nonstandard position;

*a fortiori*they will agree at each

*i*-th position for

*i*∈ℕ. But we have, as a theorem of PA, that the bitstring

*n*can be truncated to any desired length:

∀*k<*length(*n*) ∃*m* (length(*m*)=*k* ∧ ∀*i*<*k* [*m*]* _{i}*=[

*n*]

*)*

_{i}(This is the additional important property.) Pick a nonstandard *k*∈*M* and truncate *n* to *k* bits, computing inside *N*. Call the result *m*. Now, *m* belongs to *M* because *m*<2^{k} and *M*⊆_{e}*N*. Summing up, for all *i*<*k*, *N*⊧[*n*]* _{i}*=1 iff

*N*⊧[

*m*]

*=1 iff*

_{i}*M*⊧[

*m*]

*=1. Therefore any set coded in*

_{i}*N*is also coded in

*M*, and SSy(

*N*)⊆SSy(

*M*).