[FOM] PA and recursive saturation
Harvey Friedman
friedman at math.ohio-state.edu
Sat Mar 18 22:43:56 EST 2006
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
More information about the FOM
mailing list