In automated proving one can define the best proof of a theorem as the one which minimizes the length of the proof. Given a set of known statements one could define the difficulty of a theorem as the minimum length among all its proofs deduced from known statements. One could also define the importance of a theorem $T$ in a set of statements as the inverse of the sum of the difficulty of all the remaining theorems known $T$.
Even in a setting not as formal as automated proving these ideas seem very natural to me.
My question:
Has anyone ever elaborated a satisfactory theory of distance between/difficulty of/importance of/etc. of theorems?
"Given a set of known statements one could define the difficulty of a theorem as the minimum length among all its proofs deduced from known statements. One could also define the importance of a theorem T in a set of statements as the inverse of the sum of the difficulty of all the remaining theorems known T."
In even axiomatic propositional calculi it's known that the set of all remaining theorem is infinite. Since the difficulty of all theorems is positive for each theorem, this implies that every theorem in say 2-valued or any other axiomatic proposition calculus has an infinite importance.
You might want to think that all those remaining theorems aren't known. And in some sense that comes as correct. However, there do exist infinite patterns of theorems which are knowable in some sense. For example, under condensed detachment as a rule of inference, if CpCqp is an axiom or theorem ("thesis" hereafter), then we have this infinite pattern of theses:
{CpCqp, Cp$_1$CpCqp, Cp$_2$Cp$_1$CpCqp ... }
And you can prefix an infinite sequence of theses in a similar manner.
Another pattern is the sequence of theses derivable using condensed detachment where CCpqCCqrCpr is always the major premise in say any system where "C" is the main connective for every axiom. Since "Cpq" unifies with every axiom, and by using condensed detachment you generate a conditional of the form CC$\alpha$$\beta$C$\gamma$$\beta$, Cpq unifies with every theses in this sequence. Using D notation it goes (1, D1.1 = 2, D1.2 = 3, D1.3 = 4...) Another knowable pattern of theses starts with CCpqCCrpCrq and behaves similarly to the previous pattern.
Robert Veroff did some work on finding shortest proofs in propositional calculi systematically (Larry Wos has spent years searching for short proofs with theorem provers, but there exist very few proofs which have seem to have gotten proved to be the shortest). You might want to see his paper which you can get read in Postscript format as his website:
Finding Shortest Proofs: An Application of Linked Inference Rules