[FOM] PA and recursive saturation

[A.S.Virdi@lse.ac.uk]

In Chapter 15 ('Recursive Saturation') of Richard Kaye's 1991 "Models of Peano Arithmetic", Kaye demonstrates the following: (roughly) take the system known as PA(S) - an extension of the language of Peano Arithmetic by adding a satisfaction predicate governed by the Tarskian axioms - and disallow the extended langauge to feature in the inductive reasoning of this theory. Call this theory PA(S)_0. Kaye shows in this chapter that any countable model of Peano Arithmetic can be extended to a recursively saturated model of PA(S)_0. From this it follows that PA(S)_0 is a conservative extension of PA. In fact, this result was first established by Kotlarski, Krajewski & Lachlan in 1981. 

Does anyone on the list know of a proof-theoretic correlate to this conservativeness result?

Best regards --- Arhat Virdi, L.S.E.