# Is it possible to assign an objective profundity to theorems in a formal system?

To be concrete and specific, let us say we are working in Peano Arithmetic. Is it possible to assign a partial order among theorems of Peano Arithmetic that agrees with our vague intuitive notion of profundity? So for instance, "0=0" would be ranked less than "SS0+SS0=SSSS0", and both would be ranked less than "For all x and y, (x+y)=(y+x)". What I am really asking for is if there is any text on this or a similar line of thought. I would love to read such a text.

• is profundity the right word?
– user6917
Commented Sep 5, 2014 at 14:36
• Your example regards the lenght of the formulae, i.e.the number of symbols; I think this is not meaningful. Sometimes it cab be used the rank of a formula, i.e. the number of leading quantifiers. Very important is the Arithmetical hierarchy which "classifies certain sets based on the complexity of formulas that define them." Commented Sep 5, 2014 at 15:16
• @MauroALLEGRANZA Oh, length is only incidental. There are long formulas that are not intuitively that profound. Such as "SSSSSSSSSSSSSS0+SS0=SSSSSSSSSSSSSSSS0". I would definitely call that less profound than a theorem like the commutativity of addition. Commented Sep 5, 2014 at 16:12
• What about taking the length of the shortest proof? Commented Sep 5, 2014 at 23:41
• But I think all this "measure" are about some sort of "complexity"; they not involve somithing like "informativeness" or "difficulty" or ... which can be the possible elucidations of profundity. Commented Sep 6, 2014 at 17:10