Stuart_Armstrong comments on Bounded versions of Gödel's and Löb's theorems - Less Wrong

32 Post author: cousin_it 27 June 2012 06:28PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (21)

You are viewing a single comment's thread.

Comment author: Stuart_Armstrong 28 June 2012 12:14:43PM *  1 point [-]

I like (apart from the use of T and S to denote very different things). EDIT: and R!

One question: any idea how long it would take T to prove S under this reasoning?

Comment author: cousin_it 28 June 2012 12:33:34PM *  0 points [-]

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.