I was wondering if inside an axiomatic theory it could be possible to assign each theorem a number that indicates its complexity.
Theorems with small complexity numbers would be "almost axioms"; if one uses a theorem with high complexity number in a proof, the resulting theorem would have a high complexity number as well.
My thought is that, given a theorem, we take a look at its proof and sum up the complexity numbers of the passages; axioms would have complexity 1 (or even 0), as well as logical operations. If a theorem has many proofs we choose the minimum.
We could go a step further. Let say we assign a complexity number also to the statements: then we would have the absolute complexity of a theorem (the one mentioned before) and the relative complexity (the ratio between the complexities of the proof and of the statement).
Do you if anything has already been done about this? Do you think that a complexity number could be actually defined in a rigorous way? If not, where would we find obstacles?
Feel free to deal with special cases or to generalize.
In theoretical computer science, this is studied. It's usually restricted to propositional logical proofs though, as those are easier to analyze. Usually it's specifically applied to proving that something is not true.
It is a very hard field to study, and the main question is whether a method can always produce a proof of size polynomial in the size of the formula. If such a method exists, then NP would be equal to coNP.
The field is called Computational Proof Complexity.