[FOM] PA and recursive saturation: correction
avigad at cmu.edu
Thu Mar 23 06:17:26 EST 2006
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.
More information about the FOM