**MW:** Last time we learned about the “back-and-forth” condition for two countable structures *M* and *N* for a (countable) language *L*:

For all *n*, given any elements *a*_{1},…,*a _{n}*∈

*M*and corresponding elements

*b*

_{1},…,

*b*∈

_{n}*N*, if the (parameter-free)

*n*-types are the same:

{φ(*x*_{1},…,*x _{n}*)∈

*L*:

*M*⊧φ(

*a*

_{1},…,

*a*)} = {φ(

_{n}*x*

_{1},…,

*x*)∈

_{n}*L*:

*N*⊧φ(

*b*

_{1},…,

*b*)}

_{n}then for any *a*∈*M* there is a *b*∈*N* so the 1-types of *a* and *b* with corresponding parameters (*a _{i}*) and (

*b*) are the same:

_{i}{φ(*x*,*x*_{1},…,*x _{n}*)∈

*L*:

*M*⊧φ(

*a*,

*a*

_{1},…,

*a*)} = {φ(

_{n}*x,*

*x*

_{1},…,

*x*)∈

_{n}*L*:

*N*⊧φ(

*b*,

*b*

_{1},…,

*b*)}

_{n}and vice versa, with the roles of *M* and *N* and the *a’*s and *b’*s switched.

When that holds, you can use the back-and-forth method to construct an isomorphism between *M* and *N*. We noted that the *n*=0 case is Th(*M*)=Th(*N*), i.e., *M* is elementarily equivalent to *N*.

Using this, we want to show that any two countable recursively saturated models *M* and *N* of PA are isomorphic if Th(*M*)=Th(*N*) and SSy(*M*)=SSy(*N*). First question: how do the standard systems SSy(*M*) and SSy(*N*) get into the act?

The basic idea: go “up, over, and down”. That is:

Using recursive saturation, we code a type in *M*. That gives us an element of SSy(*M*). Since SSy(*M*)=SSy(*N*), we’ve traversed two of links. Finally we have to translate the element of SSy(*N*) down to a type in *N*, again using recursive saturation. That’s the roadmap.

I recapped *n*-types in post 25, so I won’t go over all that again. Just a brief reminder about what ‘recursive’ means for them. The *n*-type {φ* _{i}*(

*x*

_{1},…,

*x*,

_{n}*e*

_{1},…,

*e*) :

_{k}*i*∈ℕ} with parameters

*e*

_{1},…,

*e*is

_{k}*recursive*if the set of Gödel numbers {⌜φ

*(*

_{i}*x*

_{1},…,

*x*,

_{n}*y*

_{1},…,

*y*)⌝ :

_{k}*i*∈ℕ} is recursive (with the

*y*variables replacing the

*e*parameters).

The *n*-type of elements *a _{1},…,a_{n}* (with or without parameters) unfortunately won’t always be recursive—Truth is Undefinable! We get around this with what I call the ‘equivalence trick’. Instead of the set

{φ(*x*_{1},…,*x _{n}*) :

*M*⊧ φ(

*a*

_{1},…,

*a*)}

_{n}we start with a recursive enumeration of all formulas of L(PA) with the free variables *x*_{1},…,*x _{n}*, say {ψ

*(*

_{i}*x*

_{1},…,

*x*) :

_{n}*i*∈ℕ}. Then we look at the set of formulas

{[*u*]* _{i}* =1 ↔ ψ

*(*

_{i}*a*

_{1},…,

*a*) :

_{n}*i*∈ℕ}

where *u* is a variable; if *u*=*c* realizes this set, then *c* will be the intended code. (Recall that [*c*]* _{i}* is the

*i-*th bit of

*c*, when

*c*is written in binary.) The set of Gödel numbers

{⌜[*u*]* _{i}* =1 ↔ ψ

*(*

_{i}*x*

_{1},…,

*x*)⌝ :

_{n}*i*∈ℕ}

is recursive because {ψ* _{i}*} is a recursive enumeration. Since

*M*is recursively saturated, our set will be realized for a given choice of parameters

*a*

_{1},…,

*a*, provided that every finite subset (with those parameters) is realized. But what does it mean to be realized by

_{n}*u*=

*c*? Just that the bits of the binary expansion for

*c*agree with the truth values of “

*M*⊧ψ

*(*

_{i}*a*

_{1},…,

*a*)” at the required places. Obviously we can find a

_{n}*c*that’s good for any finite number of

*i*’s. By recursive saturation, there is a

*c*that works for

*all*

*i*∈ℕ.

Apply this to the back-and-forth condition. We want to add an *a* at the front of the list of *a _{i}*’s, but this doesn’t affect the reasoning. For any

*a*,

*a*

_{1},…,

*a*∈

_{n}*M*we have a code

*c*∈

*M*for the type of

*a*,

*a*

_{1},…,

*a*, in the sense that

_{n}*M*⊧[*c*]* _{i}* =1 ⇔

*M*⊧ψ

*(*

_{i}*a*,

*a*

_{1},…,

*a*)

_{n}Say *S* is the set {*i*∈ℕ : [*c*]* _{i}* =1}. Since SSy(

*M*)=SSy(

*N*),

*S*also belongs to SSy(

*N*), and so there is a

*d*∈

*N*that codes it.

We want to show that the set

{[*d*]* _{i}* =1 ↔ ψ

*(*

_{i}*x*,

*b*

_{1},…,

*b*) :

_{n}*i*∈ℕ}

is realized in *N* by some *x*=*b*. In other words, *N*⊧ψ* _{i}*(

*b*,

*b*

_{1},…,

*b*) ⇔

_{n}*N*⊧[

*d*]

*=1. This will insure that the types of (*

_{i}*a*,

*a*

_{1},…,

*a*) in

_{n}*M*and (

*b*,

*b*

_{1},…,

*b*) in

_{n}*N*are the same. Since

*N*is recursively saturated, and the set {⌜[

*u*]

*=1 ↔ ψ*

_{i}*(*

_{i}*x*,

*x*

_{1},…,

*x*)⌝ :

_{n}*i*∈ℕ} is recursive, it’s enough to show that the set is finitely satisfiable. In other words, for any finite set

*I*⊂ℕ, there is a

*b*∈

*N*such that

*N *⊧ ⋀_{i∈I} ( [*d*]* _{i}* =1 ↔ ψ

*(*

_{i}*b*,

*b*

_{1},…,

*b*) )

_{n}Or in other words,

*N *⊧ ∃*x* ⋀_{i∈I} ( [*d*]* _{i}* =1 ↔ ψ

*(*

_{i}*x*,

*b*

_{1},…,

*b*) )

_{n}Or splitting *I* up into the positions where [*d*]* _{i}* =1 and where [

*d*]

*=0, say*

_{i}*I*=

*J*⊔

*K*:

*N *⊧ ∃*x* ( ⋀_{i∈J} ψ* _{i}*(

*x*,

*b*

_{1},…,

*b*) ∧ ⋀

_{n}_{i∈K}¬ψ

*(*

_{i}*x*,

*b*

_{1},…,

*b*) )

_{n}But the *n*-type of (*b*_{1},…,*b _{n}*) records the truth or falsity of this ∃

*x*(foo) sentence. And the

*n*-type of (

*b*

_{1},…,

*b*) is inductively assumed to equal the

_{n}*n*-type of (

*a*

_{1},…,

*a*). So the corresponding assertion about

_{n}*M*,

*M *⊧ ∃*x* ( ⋀_{i∈J} ψ* _{i}*(

*x*,

*a*

_{1},…,

*a*) ∧ ⋀

_{n}_{i∈K}¬ψ

*(*

_{i}*x*,

*a*

_{1},…,

*a*) )

_{n}is true by the way *c* was obtained. So our set {[*d*]* _{i}* =1 ↔ ψ

*(*

_{i}*x*,

*b*

_{1},…,

*b*) :

_{n}*i*∈ℕ} is finitely satisfiable—done, Done, and DONE!

(The ‘done’ is for finite satisfiability, the ‘Done’ is for the result of this section, and the ‘DONE’ is for Enayat’s Theorem 7.)

It’s been a long road.

**JB:** Hurrah! I apologize for being so quiet, much like Socrates’ partners in Plato’s later dialogues It will take me a while to catch up. But congratulations: this whole series will be go-to reading for anyone who wants to understand nonstandard models of arithmetic.