[FOM] PA and recursive saturation: correction

[Jeremy Avigad]

Responding to a posting of Arhat Virdi, on March 19 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.

...

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

I responded that this is straightforwardly provable using techniques 
described by Pudlak in his article in the Handbook of Proof Theory.

I was too glib. Harvey has pointed out to me that the argument I had in 
mind does not work when T is PA. In that case, I suspect the claim is 
false; with care, it should be possible to use reflection in PA and 
eliminate the sat predicate without significant blowup.

I think my argument works in the finitely axiomatized case, though. That 
is, I think the following theorem and sketch of a proof are correct.

Theorem. Let T be any consistent, finitely axiomatized theory in the 
language of arithmetic that extends IDelta_0 + (exp) + "iterated 
exponentiation is total". Let T(sat) be as above. Then there is a 
sequence <psi_n> of formulas with polynomial-size proofs in T(sat), but 
with no proofs of size less than 2_n^0 in T (where 2_n^x denotes n-times 
iterated exponentiation with base 2).

As a corollary, one can replace "extends" by "is consistent with" in the 
statement of the theorem. Just let theta be a finite axiomatization of 
IDelta_0 + (exp) + "iterated exponentiation is total" and use theta -> 
psi_n in place of psi_n.

To prove the theorem, use sat to obtain a formula phi(x) in the language 
of T(sat) that says "if d is any proof in T with at most x symbols, then 
the (universal closure of the) conclusion of d is true."

I claim that T(sat) proves phi(x) -> phi(x+1). This is because the 
properties of sat are enough to show that each axiom of first-order 
logic is true, each rule of inference is valid, and each of the finitely 
many axioms of T is true. So if d is a proof of a false conclusion in T, 
the subproof of one of the hypotheses of the last inference is a shorter 
proof of a false conclusion.

Note that T(sat) doesn't have induction for phi. But using Solovay's 
methods, described in Pudlak's article, T(sat) has proofs of phi(2_n^0) 
with length polynomial in n, where 2_n^0 is expressed using a 
formalization of iterated exponentiation.

Now, for each n, use the fixed-point lemma to get a formula psi_n in the 
language of T that says "I cannot be proved in T with a proof of length 
less than 2_n^0." Using the facts established above, T(sat) can carry 
out the usual proof of psi_n with a proof whose length is polynomial in 
n, but psi_n cannot be proved in T with a proof of length less than 2_n^0.

I'd appreciate hearing if anyone sees a problem with this argument.