**MW: **Continuing the recap…

Enayat defines an axiom system PA+Φ* _{T}* in the language of PA. Φ

*is the set of formulas of the form*

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

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

*n*∈ℕ}

(*T _{n}* is the first

*n*statements of

*T*, while φ

^{ℕ}is φ∈L(PA) translated into a formula of L(ZF).) Informally, “If an arithmetic statement holds in a model of

*T*, then it is consistent with

*T*.” The contrapositive form also sheds light:

{“*T _{n}*⊢φ

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

*n*∈ℕ}

Informally, “If *T* proves an arithmetic statement, then it holds in any model of *T*.”

Here are Enayat’s two big results and a corollary:

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

Theorem 7:Every countable recursively saturated model of PA+Φis a_{T}T-standard model of PA.

Corollary 8:The following statements are equivalent for a countable nonstandard modelAof arithmetic:

Ais aT-standard model of PA.Ais a recursively saturated model of PA+Φ._{T}

Φ* _{T}* captures everything that

*T*can prove about its omega

*that can be expressed in*L(PA). But that’s not enough to make a model of PA

*T*-standard. John summed up the situation nicely at the end of post 19:

You know the British phrase ‘bog-standard’? It means “utterly basic, ordinary, unremarkable, unexceptional”. … [W]henever I hear ‘ZF-standard’ or ‘V-standard’ I think about this phrase. In a way, Enayat is saying ZF-standard models of arithmetic are either extremely rich or they’re

bog-standard.

We got through the proof of the direct theorem (Prop. 6), but not the (partial) converse (Thm. 7).

For Prop.6, an overspill argument lies at the heart of proving recursive saturation. Glossing over two issues, ∃*x*⋀_{1≤i≤k} φ* _{i}*(

*x*,

*c*) holds for any standard

*k*, so by overspill it holds for some non-standard

*k*. Let

*a*be a suitable value for

*x*. But then

*a fortiori*φ

*(*

_{i}*a*,

*c*) holds for all

*i*∈ℕ.

First issue: the Tarski Truth Maze. (I call it that because it is kind of amazing, and because it took us a while to get through it.) We need ∃*x*⋀_{1≤i≤k} φ* _{i}*(

*x*,

*c*) to be expressible via a single formula, with

*k*as a variable in the language, not a “meta-variable”. But ZF has a definable truth predicate for arithmetic statements—say, True(⌜φ

^{ℕ}⌝ ). So we let

ψ(*k*) ≡ True(⌜∃*x*⋀_{1≤i≤k} φ* _{i}*(

*x*,

*c*)

^{ℕ}⌝)

and apply overspill to ψ.

Second issue: the parameter *c*. I made a point in the previous post that with a recursive type, you *begin* with a recursive set of formulas {φ* _{i}*(

*x,y*) :

*i*∈ℕ} in L(PA), and

*then*plug in

*c*. In what sense is ⌜∃

*x*⋀

_{1≤i≤k}φ

*(*

_{i}*x*,

*c*)

^{ℕ}⌝ a recursive function of

*k*? Note first that for

*standard k*and

*c*, ∃

*x*⋀

_{1≤i≤k}φ

*(*

_{i}*x*,

*c*)

^{ℕ}is a formula in L(ZF), and pretty clearly its Gödel number is a recursive function of the pair (

*k*,

*c*). Recursive functions can be represented in L(ZF), so we have a formula in L(ZF)

ψ(*k,y*) ≡ True(⌜∃*x*⋀_{1≤i≤k} φ* _{i}*(

*x*,

*y*)

^{ℕ}⌝)

and we’re good to go.

Here is the argument for Prop. 6, spelled out: Suppose the recursive set of formulas {φ* _{i}*(

*x*,

*y*)} is finitely satisfiable in ω

^{U}for some particular

*y*=

*c*. Therefore

*U*⊧ψ(

*k,c*) for all standard

*k*, so

*U*⊧ψ(

*k,c*) for some nonstandard

*k*, so for some

*a*∈ω

^{U},

*U*⊧True(⌜⋀

_{1≤i≤k}φ

*(*

_{i}*a*,

*c*)

^{ℕ}⌝). So

*U*⊧φ

*(*

_{i}*a*,

*c*)

^{ℕ}for all

*i*≤

*k*,

*a fortiori*for all standard

*i*, and finally ω

^{U}⊧φ

*(*

_{i}*a*,

*c*) for all all standard

*i*. Thus ω

^{U}is recursively saturated in the real world. Done.

Kaye’s Theorem 11.5 (p.150) proves that every nonstandard model of PA is recursively Σ_{n}-saturated by a similar argument. He uses the Σ_{n} satisfaction predicate instead of the ZF-based one. His ψ(*k,y*) is a variation on ours, and (with the ZF truth predicate) would also work here. You might prefer it. The basic idea: say *S* is the set of Gödel numbers of a recursive Σ_{n}-type. Code *S* with a nonstandard number *s*. This allows us to say formally “⌜φ* _{i}*(

*x*,

*y*)⌝ ∈

*S”*, plugging

*s*into a formula of L(PA). Kaye’s version of ψ(

*k,c*) then looks something like this (with

*j*being ⌜φ

*(*

_{i}*x*,

*y*)⌝):

ψ(*k,c*) ≡ ∃*x*∀*j*≤*k *(*j*∈*S* → Sat_{Σn}(*j*,*c*))

Sat_{Σn}(⌜φ* _{i}*(

*x*,

*y*)⌝,

*c*) formally expresses “φ

*(*

_{i}*x*,

*y*) is Σ

_{n}, and φ

*(*

_{i}*x*,

*y*) is true when you plug in

*c*for

*y”*.

So that’s last season on Nonstandard Models of Arithmetic! Stay tuned.