[FOM] Question on Equivalence of Theorems

[Harvey Friedman]

>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
>
>_______________________________________________
>FOM mailing list
>FOM at cs.nyu.edu
>http://www.cs.nyu.edu/mailman/listinfo/fom

You should become familiar with Reverse Mathematics, if you aren't 
already, a highly developed part of f.o.m. Steve Simpson wrote the 
definitive book on it, published by Springer in 1999.

There has been a lot of discussion about reverse mathematics, and if 
we had the old search engine for the archives, you could search there 
on "reverse mathematics". I understand that the moderator is trying 
to get such a search engine attached to the archives.