have people ever formalized the intuition that some truths are true for more complicated reasons than others?
like... if the minimum formal proof of Fermat's last theorem is really really long, does that... mean anything?
Conversation
so, you can write down a function l(P) that given a proposition P in some formal system outputs the length of the shortest proof of P (and maybe throws an error if P isn't provable or something). and you can consider L(n), the maximum of l(P) over all statements P of length n
1
6
for reasonably powerful formal systems, eg peano arithmetic, L(n) grows faster than any computable function!
because if it was bounded by a computable function then you could use that function to determine which statements are provable (by checking all proofs up to that length)
2
4
so there are statements that aren't too long but have insanely long proofs, which you might argue is a reasonable formalization of "true for really complicated reasons," depending on the strength of the formal system
1
5
whether this applies to any particular statement is unclear b/c it's quite hard to search over the entire space of proofs. and in any case the sort of proofs that humans read are not the sort of proofs that we formally reason about
2
2
so, two thoughts. one is that we can e.g. compare what peano arithmetic and ZFC have to say about arithmetic, by "encoding" arithmetic in ZFC, as consisting of the statements ZFC can prove about the natural numbers and addition etc. as defined in ZFC
1
3
another is a more general procedure called "ordinal analysis" where you can, loosely speaking, sort theories by which ordinals they can prove exist, or something like that, i'm not familiar with the details:
2
2
the whole thing has a kind of shonen anime "it's over 9000" flavor lol
(i think i stole this joke from eliezer but i forget)