Yes, you need to have a theory of physics to write down a transition rule for a physical system. That is a problem, but it’s not at all the same problem as the “target format” problem. The only role the transition rule plays here is it allows one to apply induction to efficiently prove some generalization about the system over all time steps.
In principle a different more distinguished concise description of the system’s behaviour could play the a similar role (perhaps, the recording of the states of the system + the shortest program that outputs the recording?). Or perhaps there’s some way of choosing a distinguished “best” formalization of physics. But that’s rather out of scope of what I wanted to suggest here.
But then you are measuring proof shortness relative to that system. And you could be using one of countless other formal systems which always make the same predictions, but relative to which different proofs are short and long.
It would be a O(1) cost to start the proof by translating the axioms into a more convenient format. Much as Kolmogorov complexity is “language dependent” but not asymptotically because any particular universal turing machine can be simulated in any other for a constant cost.
The assumption (including that it takes in and puts out in arabic numerals, and uses “*” as the multuplication command, and that buttons must be pressed,… and all the other things you need to actually use it) includes that.
These are all things that can be derived from a physical description of the calculator (maybe not in fewer steps than it takes to do long multiplication, but certainly in fewer steps than less trivial computations one might do with a calculator). There’s no observer dependency here.
It would be a O(1) cost to start the proof by translating the axioms into a more convenient format. Much as Kolmogorov complexity is “language dependent” but not asymptotically because any particular universal turing machine can be simulated in any other for a constant cost.
And the thing that isnt O(1) is to apply the transition rule until you reach the relevant time step, right? I think I understand it now: The calculations involved in applying the transition rule count towards the computation length, and the simulation should be able to answer multible questions abouth the thing it simulates. So if object A simulates object B, we make a model X of A, prove it equivalent to the one in our theory of physics, then prove it equivalent to your physics model of B, then calculate forward in X, then translate the result back into B with the equivalence. And then we count the steps all this took. Before I ask any more questions, am I getting that right?
Yes, you need to have a theory of physics to write down a transition rule for a physical system. That is a problem, but it’s not at all the same problem as the “target format” problem. The only role the transition rule plays here is it allows one to apply induction to efficiently prove some generalization about the system over all time steps.
In principle a different more distinguished concise description of the system’s behaviour could play the a similar role (perhaps, the recording of the states of the system + the shortest program that outputs the recording?). Or perhaps there’s some way of choosing a distinguished “best” formalization of physics. But that’s rather out of scope of what I wanted to suggest here.
It would be a O(1) cost to start the proof by translating the axioms into a more convenient format. Much as Kolmogorov complexity is “language dependent” but not asymptotically because any particular universal turing machine can be simulated in any other for a constant cost.
These are all things that can be derived from a physical description of the calculator (maybe not in fewer steps than it takes to do long multiplication, but certainly in fewer steps than less trivial computations one might do with a calculator). There’s no observer dependency here.
And the thing that isnt O(1) is to apply the transition rule until you reach the relevant time step, right? I think I understand it now: The calculations involved in applying the transition rule count towards the computation length, and the simulation should be able to answer multible questions abouth the thing it simulates. So if object A simulates object B, we make a model X of A, prove it equivalent to the one in our theory of physics, then prove it equivalent to your physics model of B, then calculate forward in X, then translate the result back into B with the equivalence. And then we count the steps all this took. Before I ask any more questions, am I getting that right?