That’s not an issue in my formalization. The “logical facts” I speak of in the formalized version would be fully specified mathematical statements, such as “if the simulation starts in state X at t=0, the state of the simulation at t=T is Y” or “given that Alice starts in state X, then <some formalized way of categorising states according to favourite ice cream flavour> returns Vanilla”. The “target format” is mathematical proofs. Languages (as in English vs Chinese) don’t and can’t come in to it, because proof systems are language-ignorant.
Note, the formalized criterion is broader than the informal “could you do something useful with this simulation IRL” criterion, even though the latter is the ‘inspiration’ for it. For instance, it doesn’t matter whether you understand the programming language the simulation is written in. If someone who did understand the language could write the appropriate proofs, then the proofs exist.
Similarly, if a simulation is run under Homomorphic_encryption, it is nevertheless a valid simulation, despite the fact that you can’t read it if you don’t have the decryption key. Because a proof exists which starts by “magically” writing down the key, proving that it’s the correct decryption key, then proceeding from there.
An informal criterion which maybe captures this better would be: If you and your friend both have (view) access to a genuine computation of some logical facts X, it should be possible to convince your friend of X in fewer words by referring to the alleged computation (but you are permitted unlimited time to think first, so you can reverse engineer the simulation, bruteforce some encryption keys, learn Chinese, whatever you like, before talking). A bit like how it’s more efficient to convince your friend that 637265729567*37265974 = 23748328109134853258 by punching the numbers into a calculator and saying “see?” than by handing over a paper with a complete long multiplication derivation (assuming you are familiar with the calculator and can convince your friend that it calculates correctly).
In that case, the target format problem shows up in the formalisation of the physical system.
A specific formalization of this idea would be that a proof system equipped with an oracle (axiom schema) describing the states of the physical system which allegedly computed these facts, as well as its transition rule, should be able to find proofs for those logical facts in less steps than one without such axioms.
Such proofs will involve first coming up with a mapping (such as interpreting certain electrical junctions as nand gates), proving them valid using the transition rules, then using induction to jump to “the physical state at timestep t is X therefore Alice’s favourite ice cream colour is Y”.
How do you “interpret” certain electrical junctions as nand gates? Either you already have
a proof system equipped with an axiom schema describing the states of the physical system, as well as its transition rule
or this is a not fully formal step. Odds are you already have one (your theory of physics). 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. To steal someone elses explanation:
Let us imagine a white surface with irregular black spots on it. We then say that whatever kind of picture these make, I can always approximate as closely as I wish to the description of it by covering the surface with a sufficiently fine square mesh, and then saying of every square whether it is black or white. In this way I shall have imposed a unified form on the description of the surface. The form is optional, since I could have achieved the same result by using a net with a triangular or hexagonal mesh. Possibly the use of a triangular mesh would have made the description simpler: that is to say, it might be that we could describe the surface more accurately with a coarse triangular mesh than with a fine square mesh (or conversely), and so on.
And which of these empirically indistinguishable formalisations you use is of course a fact about the map. In your example:
A bit like how it’s more efficient to convince your friend that 637265729567*37265974 = 23748328109134853258 by punching the numbers into a calculator and saying “see?” than by handing over a paper with a complete long multiplication derivation (assuming you are familiar with the calculator and can convince your friend that it calculates correctly).
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.
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?
That’s not an issue in my formalization. The “logical facts” I speak of in the formalized version would be fully specified mathematical statements, such as “if the simulation starts in state X at t=0, the state of the simulation at t=T is Y” or “given that Alice starts in state X, then <some formalized way of categorising states according to favourite ice cream flavour> returns
Vanilla”. The “target format” is mathematical proofs. Languages (as in English vs Chinese) don’t and can’t come in to it, because proof systems are language-ignorant.Note, the formalized criterion is broader than the informal “could you do something useful with this simulation IRL” criterion, even though the latter is the ‘inspiration’ for it. For instance, it doesn’t matter whether you understand the programming language the simulation is written in. If someone who did understand the language could write the appropriate proofs, then the proofs exist.
Similarly, if a simulation is run under Homomorphic_encryption, it is nevertheless a valid simulation, despite the fact that you can’t read it if you don’t have the decryption key. Because a proof exists which starts by “magically” writing down the key, proving that it’s the correct decryption key, then proceeding from there.
An informal criterion which maybe captures this better would be: If you and your friend both have (view) access to a genuine computation of some logical facts X, it should be possible to convince your friend of X in fewer words by referring to the alleged computation (but you are permitted unlimited time to think first, so you can reverse engineer the simulation, bruteforce some encryption keys, learn Chinese, whatever you like, before talking). A bit like how it’s more efficient to convince your friend that 637265729567*37265974 = 23748328109134853258 by punching the numbers into a calculator and saying “see?” than by handing over a paper with a complete long multiplication derivation (assuming you are familiar with the calculator and can convince your friend that it calculates correctly).
In that case, the target format problem shows up in the formalisation of the physical system.
How do you “interpret” certain electrical junctions as nand gates? Either you already have
or this is a not fully formal step. Odds are you already have one (your theory of physics). 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. To steal someone elses explanation:
And which of these empirically indistinguishable formalisations you use is of course a fact about the map. In your example:
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.
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?