# 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 Sep 5 '14 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." – Mauro ALLEGRANZA Sep 5 '14 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. – user107952 Sep 5 '14 at 16:12
• What about taking the length of the shortest proof? – Tim kinsella Sep 5 '14 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. – Mauro ALLEGRANZA Sep 6 '14 at 17:10