MW: Continuing the recap…
Enayat defines an axiom system PA+ΦT in the language of PA. ΦT is the set of formulas of the form
{φ → Con(Tn+φℕ) : φ∈L(PA), n∈ℕ}
(Tn 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:
{“Tn⊢φℕ” → φ : φ∈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+Φ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.
Φ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.
Diagonal Argument 