I’m not sure this would work, and it might be tied to ambiguity about what “steps” mean.
Consider:
Y: Run X to completion. Then say “no” to chocolate.
Then PA proves that Y doesn’t lose in less steps than X (since X doesn’t do anything in more than N steps while Y runs N+1 steps before taking action), yet it’s clear that Y loses.
I think it’s because “lose in n steps” is not clear.
It doesn’t mean computation steps. Losing in 1 step means you say “no” to chocolate, losing in 2 steps means you accept some program that says “no” to chocolate, and so on. Sorry, I thought that was the obvious interpretation, I’ll edit the post to make it clear.
I’m not sure this would work, and it might be tied to ambiguity about what “steps” mean.
Consider:
Y: Run X to completion. Then say “no” to chocolate.
Then PA proves that Y doesn’t lose in less steps than X (since X doesn’t do anything in more than N steps while Y runs N+1 steps before taking action), yet it’s clear that Y loses.
I think it’s because “lose in n steps” is not clear.
It doesn’t mean computation steps. Losing in 1 step means you say “no” to chocolate, losing in 2 steps means you accept some program that says “no” to chocolate, and so on. Sorry, I thought that was the obvious interpretation, I’ll edit the post to make it clear.
Ah, thanks! That seems more sensible.