Kindly 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. Show more comments above.

Comment author: Kindly 28 June 2012 12:49:47AM 1 point [-]

How do we know what the proof by simulation does in exp(g(n)) symbols, if the length of our argument is linear in n?

Comment author: cousin_it 28 June 2012 01:16:51AM *  1 point [-]

Exhibiting the complete proof by simulation is not necessary, I think. It's enough to prove that it exists, that its length is bounded, and that it must contradict the proof found by R. All these statements have simple proofs by inspection of R.