Kindly 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)
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?
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.