**JB:** It’s been a long time since Part 11, so let me remind myself what we’re talking about in Enayat’s paper Standard models of arithmetic.

We’ve got a theory *T* that’s a recursively axiomatizable extension of ZF. We can define the ‘standard model’ of PA in any model of *T*, and we call this a ‘*T*-standard model’ of PA. Then, we let PA^{T} to be all the closed formulas in the language of Peano arithmetic that hold in all *T*-standard models.

This is what Enayat wants to study: the stuff about arithmetic that’s true in all *T*-standard models of the natural numbers. So what does he do first?