[FOM] Question on Equivalence of Theorems

[Robin Adams]

Mathematicians often talk of two theorems being equivalent, or one being
stronger or weaker than another.  This cannot mean logical equivalence or
strength; any two theorems are logically equivalent, since both are true.
Nor does it seem to be anything related to proof theoretic strength.

`Theorems T1 and T2 are equivalent' seems to mean that there is a simple
derivation of T2 from T1 and vice versa; smipler than any proof of the
theorem from scratch (i.e. the axioms).  `Stronger' and `Weaker' indicates
that there is such a proof in one direction, but not the other.

Has this notion ever been formalised in proof theory?  I have in mind the
assignment of a level of compexity to proofs and derivations; then a
definition along the lines of

`T1 and T2 are equivalent iff there are complexity 0 derivations of T2
from T1 and vice versa'

or

`T1 and T2 are equivalent iff there are derivations of T2 from T1 and vice
versa of complexity <= n, while every proof of T1 and T2 is of complexity
>n.'

-- 
Robin Adams