[FOM] Lengths of proofs 1
Harvey Friedman
friedman at math.ohio-state.edu
Sun Feb 12 02:33:32 EST 2006
Let us start with the system T0 whose language is 0,S,R, where S is a unary
function symbol and R is a unary predicate symbol. We write n* for S...S(0),
where there are n S's. Equality is assumed.
The axioms of T0
R0.
(forall x)(Rx implies RSx).
Apparently, there is a cut free proof of Rn* where the number of atomic
formulas, connectives, and quantifiers, used do not significantly blow up as
a function of n.
I would guess that the total number of symbols appearing in a proof in T0 of
Rn*, excluding parentheses, should be at least n, even if cuts are allowed.
Also, it seems reasonable that the length of any proof from T0 of Rn* should
be at least n (depth of proof tree), even if cuts are allowed.
These results should remain the same if we use T1 =
R0.
(forall x)(Rx implies RSx).
(forall x)(not Sx = 0).
(forall x,y)(Sx = Sy implies x = y).
Now let the language of T2 be the language of T0 together with +. The axioms
of T1 are
R0.
(forall x)(Rx implies RSx).
(forall x,y)(x + 0 = 0 and x + Sy = S(x + y)).
In T2, using addition, we have an obvious natural definition of 2^n, with n
existential quantifiers. Call this definition n#.
We can prove P(n#) in T2 with a proof with cut, with no significant blowup
over n. I would guess that we need at least length n under various measures,
even with cut. I haven't investigated the situation without cut.
The results should remain the same if we add those two successor axioms
above.
There are a number of ways of interpreting such results along these lines.
One is "arithmetic without induction".
To be continued.
Harvey Friedman
More information about the FOM
mailing list