[FOM] Lengths of proofs 1

[Harvey Friedman]

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