[FOM] PA and recursive saturation

[Harvey Friedman]

On 3/9/06 5:55 AM, "A.S.Virdi at lse.ac.uk" <A.S.Virdi at lse.ac.uk> wrote:

Your posting is not very readable in the Archives because of margin
problems. So I reproduce your entire post here.

Your post has already received a response by Avigad at
http://www.cs.nyu.edu/pipermail/fom/2006-March/010172.html
 
> 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?
> 

Let T be any reasonable theory, finitely axiomatized like ISigma1, or
schematically like PA. We can form T(sat) as you indicate.

One can give a proof of the conservativity of T(sat) over T for all formulas
in L(T), by a cut elimination argument. This argument will establish that
any proof in T(sat) of a formula in L(T) can be converted to a proof in T of
that same formula, whose number of symbols is bounded by a stack of 2's
whose height is linear in the number of symbols of the original proof in
T(sat). 

It also appears that for reasonable T, there is a superexponential blowup
here. Is this known?

Harvey Friedman