[FOM] PA and recursive saturation

[Jeremy Avigad]

Arhat Virdi wrote:

> 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?

As I recall, the theory PA(S)_0 is easily interpreted in the subsystem 
of second-order arithmetic known as Sigma^1_1-AC_0. The model-theoretic 
construction also shows that Sigma^1_1-AC_0 is conservative over PA for 
Pi^1_2 sentences. This theorem is due to Barwise and Schlipf, and 
probably also to Friedman, independently. I think the model-theoretic 
argument can be found in Steve Simpson's book.

There are straightforward syntactic proofs of these conservation 
results, using cut-elimination. A uniform model-theoretic method of 
obtaining a number of conservation results like this can be found in a 
paper of mine, "Saturated models of universal theories", on my web page, 
http://www.andrew.cmu.edu/~avigad. The paper also gives a uniform way of 
translating these model theoretic arguments to syntactic arguments, by 
appealing to normalization (or cut elimination) for first-order 
intuitionistic logic.

Jeremy