MW: Recap: we showed that PAT implies ΦT, where ΦT is the set of all formulas
Now we have to show the converse, that PA+ΦT implies PAT. But first let’s wave our hands, hopefully shaking off some intuition, like a dog shaking off water.
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 PAT 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?
MW: Time to start on Enayat’s paper in earnest. First let’s review his notation. M is a model of T, a recursively axiomatizable extension of ZF. He writes for the ω of M equipped with addition and multiplication, defined in the usual way as operations on finite ordinals. So is what he calls a T-standard model of PA.
JB: So, last time you sketched the proof of the Paris–Harrington theorem. Your description is packed with interesting ideas, which will take me a long time to absorb. Someday I should ask some questions about them. But for now I’d like to revert to an earlier theme: how questions about the universe of sets cast their shadows down on the world of Peano arithmetic.
MW: Time to talk about the Paris-Harrington theorem. Originally I thought I’d give a “broad strokes” proof, but then I remembered what you once wrote: keep it fun, not a textbook. Anyway, Katz and Reimann do a nice job for someone who wants to dive into the details, without signing up for a full-bore grad course in model theory. So I’ll say a bit about the “cast of characters” (i.e., central ideas), and why I think they merit our attention.
JB: So, you were going to tell me a bit how questions about the universe of sets cast their shadows down on the world of Peano arithmetic.
MW: Yup. There are few ways to approach this. Mainly I want to get to the Paris-Harrington theorem, which Enayat name-checks.
First though I should do some table setting of my own. There’s a really succinct way to compare ZF with PA: PA = ZF − infinity!