[FOM] PA and recursive saturation
avigad at cmu.edu
Fri Mar 10 12:33:48 EST 2006
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
More information about the FOM