[FOM] PA and recursive saturation
avigad at cmu.edu
Tue Mar 21 13:56:15 EST 2006
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
> 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.
More information about the FOM