= 27d567bc2d48d9f40e9ccc20ea370b15)
Zetetic comments on Bounded versions of Gödel's and Löb's theorems - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (21)
Could you elaborate on this? What is the slightly-more-than-n-symbols-long proof?
As I understand it, because T proves in n symbols that "T can't prove a falsehood in f(n) symbols", taking the specification of R (program length) we could do a formal verification proof that R will not find any proofs, as R only finds a proof if T can prove a falsehood within g(n)<exp(g(n)<<f(n) symbols. So I'm guessing that the slightly-more-than-n-symbols-long is on the order of:
n + Length(proof in T that R won't print with the starting true statement that "T can't prove a falsehood in f(n) symbols")
This would vary some with the length of R and with the choice of T.