= 27d567bc2d48d9f40e9ccc20ea370b15)
cousin_it comments on The limited predictor problem - 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 (7)
Thanks for the compliment ;-) but I still don't completely understand your comment. If you mean the version of A that doesn't refer to runtime(A) explicitly, what's the short proof of the second statement?
"if A()=a and runtime(A)<N then U()=u" can only be proved by an agent that represents runtime() explicitly, which means it would probably find (relatively short) general proofs of the form (max proof length)<L => runtime < some function of L,
and
agent proves X => length of proof of X < max proof length.
Although, now that I think of it more, this does not help, as in this setting the agent may easily prove X but not "agent proves X"... You're right, the proof of the second statement is not obviously short.