cousin_it 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.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (21)
I think the proof would be about g(n) symbols long, which is basically linear in n. Since R finds a proof shorter than g(n), exhibiting that proof yields a slightly longer proof that R stops early (because R either finds the exhibited proof, or stops even earlier). Then it's easy to deduce that T+¬S is inconsistent, which can be converted into a proof of S from T.