Recursive Saturation

Woo-hoo! Michael Weiss almost taught me how to prove every nonstandard model of PA is ‘recursively saturated’:

• John Baez and Michael Weiss, Non-standard models of arithmetic 20, 12 October 2020.

Suppose you have a model of Peano arithemetic. Suppose you have an infinite list of predicates in Peano arithmetic: Suppose that for any finite subset of these, your model of PA has an element making them true. Is there an element making all these predicates true?

Of course this doesn’t hold in...