When two theorems are equivalent? [Formal definition] I understand that two mathematical statements (theorems) are equivalent when one can prove any of the statements by using the other one. Is there a formalism for such a description?
 A: It depends on what's meant by "equivalent".  This can usually be determined by context, though sometimes more than one kind of equivalence is intended at once.  Here are a few varieties, which are not intended to be exhaustive.  A little reflection might also suggest that the distinctions between them are not completely sharp.  In other words, the problem of giving a formalism to disambiguate between these uses of "equivalent" would seem to require a pretty good chunk of AI.
A. Statements are said to be "materially equivalent" if either both are true or both are false.  Since all theorems are true statements, all theorems are materially equivalent.  So, it's unnatural to assert material equivalence between theorems.  
Rather, material equivalence may be asserted when two statements are known to be either both true or both false but it's not known which.  For example, 

The following are equivalent:
1a. P=NP.
2a. P=PH.

However, people may mean something else when they say "the following are equivalent".  
B. Consider a statement like
The following are equivalent:
1b. $x$ is an even prime.
2b. $x=2$.

Since the letter $x$ refers to no particular number, therefore the sentence 1b is not either true or false.  So the claim cannot be that 1b and 2b are materially equivalent.  Rather, what's presumably meant here is: 

$x$ is an even prime iff $x=2$, for all values of $x$.

So in this (very common) usage, "the following are equivalent" is shorthand for a generalization about two properties, namely that they are satisfied by exactly the same objects.
C. Now consider
The following are equivalent:
1c. The generalized continuum hypothesis.
2c. The generalized maximization principle.

This statement need not be interpreted as asserting material equivalence, because it might be found acceptable by people who doubt that 1c or 2c are either true or false at all.  Nor need it be interpretable as asserting a universally generalized biconditional.  Rather, what's meant here is a relationship of interderivability.  That is to say, the statement is rather that one can deduce 1c from 2c and vice versa.  Sometimes, the intended relationship may be simply that one sentence is derivable from the other by pure logic.  Other times, as in the case above, what's meant is that the sentences are interderivable given a certain background theory, for example the rest of the axioms of set theory.  This kind of equivalence might be understood as a statement about sentences, i.e., as genuinely metalinguistic.  
D. Finally, consider
Hall's theorem is equivalent to the marriage theorem.
This may be closest to what you have in mind.  It's probably quite nontrivial to give a general analysis of claims like this.  What might be meant is something like "each theorem can be derived from the other more easily than either can be independently proven".  Or---and this is similar---what might be meant is that an independent proof of any of them requires essentially the "same idea".  In contrast to the earlier forms of equivalence, this one is vague.  It could fruitfully be explicated in this or that way, but the choice between explications may have to be somewhat arbitrary. 
