alright just for fun: AMA but only about math, will attempt to speed-explain stuff with as few symbols and equations as possible and see what happens
(esp happy to field questions about stuff that seems basic to you and that you feel like you should've gotten a long time ago!)
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
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
Show replies