(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!
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.
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!
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.