FOM: The 'right' proof

[AndrEs Eduardo Caicedo]

My name is Andres Eduardo Caicedo, I'm a graduate student at Berkeley. My
primary interest is in Set Theory (large cardinals, forcing).

I have been thinking about something, but I'm not sure if it can be made
rigorous, or if someone has thought about it to some extent.

Is there any way to classify the relevance of a proof? An informal
discussion more than a couple of definitions is probably more enlightening
here.

For example, I took a course with John Steel this semester, roughly an
introduction to recursion theory. Consider the problem of showing that
there are two incomparable degrees.

A brute way of showing this (in fact, 'my' first proof of it) is: 
Force -CH (without collapsing w_1, say). Then, since only countably many
degrees are recursive in any given real, there are 2 incomparable. By
absoluteness results (this is were we use we didn't collapse w_1),
technically: By Schoenfield's absoluteness theorem, the same holds in
the ground model -notice "there are 2 incomparable degrees" is a
Sigma-1-1 assertion.

Ok. This is A proof, but we can argue that it is not THE proof. It does
not provide us with any relevant recursion-theoretic information (like:
there are 2 incomparable degrees below 0', or any non-0 degree is
incomparable with another), and it uses a huge machinery (forcing) to
obtain a very simple result.

Is there any *formal* way of, given a proof, detect its relevance? I am
not talking about automatic devices to check validity of proofs. Nor of
devices capable to eliminate in any proof all the irrelevant lines (if we 
unravel the proof above, there are thousands of irrelevant lines in it). A
possible approximation to a formalization of the problem can be:

"If a provable assertion has complexity G -where G=\Delta^0_n, or
\Sigma^1_1, etc-, then there is a proof of it containing only assertions
of complexity F_G", were F is definable in some way. This perhaps is
false, perhaps for obvious reasons, but I don't know. If it is true, we
are trying to measure relevance here by bounding the complexity of the
statements of the proof in terms of the complexity of the problem, so the
proof is 'close' in some sense to the problem. But perhaps there are more
accurate measures of relevance.

Any thoughts?

AndrEs Caicedo