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
Replying to
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
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
Show replies