# gRR comments on The limited predictor problem - Less Wrong

10 21 March 2012 12:15AM

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

Sort By: Best

Comment author: 21 March 2012 11:51:57AM 0 points [-]

Hmm. It seems to me, the following holds:

(agent proves "if A()=a then U()=u") => "if A()=a and runtime(A)<N then U()=u"
(agent proves "if A()=a and runtime(A)<N then U()=u") => "if A()=a then U()=u"

where the right parts are logically implied, but not necessarily proved by the agent, although in almost all cases they would be, the proof steps from one to the other being so small...

In any case, the idea of logically controlling the non-obvious properties of computation is splendid, thanks for writing it up!

Comment author: 21 March 2012 11:56:52AM *  0 points [-]

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?

Comment author: 21 March 2012 12:27:16PM 0 points [-]

"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.