**JB:** Before we get into any proofs, I’d just like to *marvel* at Enayat’s Prop. 6, and see if I understand it correctly. I tried to state it in my own words on my own blog:

Every ZF-standard model of PA that is not

V-standard is recursively saturated.