[FOM] PA and recursive saturation

[Jeremy Avigad]

Harvey Friedman wrote:

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

This is an easy consequence of the methods used to establish the 
corresponding results for e.g. GB and ZF, or ACA0 and PA. See Section 7 
of Pudlák's article in the Handbook of Proof Theory for sharp 
upper/lower bounds and references.

Jeremy