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