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