I haven’t tried as hard as I could have to understand, so, sorry if this comment is low quality.
But I currently don’t see the point of employing linear logic in the way you are doing it.
The appendix suggests that the solution to spurious counterfactuals here is the same as known ideas for resolving that problem. Which seems right to me. So solving spurious counterfactuals isn’t the novel aspect here.
But then I’m confused why you focus on 5&10 in the main body of the post, since that’s the main point of the 5&10 problem.
Maybe 5&10 is just a super simple example to illustrate things. But then, I don’t know what it is you are illustrating. What is linear logic doing for you that you could not do some other way?
I have heard the suggestion that linear logic should possibly be used to aid in the difficulties of logical counterfactuals, before. But (somehow) those suggestions seemed to be doing something more radical. Spurious counterfactuals were supposed to be blocked by something about the restrictive logic. By allowing the chosen action to be used only once (since it gets consumed when used), something nicer is supposed to happen, perhaps avoiding problematic self-referential chains of reasoning.
(As I see it at the moment, linear logic seems to—if anything—work against the kind of thing we typically want to achieve. If you can use “my program, when executed, outputs ‘one-box’” only once, you can’t re-use the result both within Omega’s thinking and within the physical choice of box. So linear logic would seem to make it hard to respect logical correlations. Of course this doesn’t happen for your proposal here, since you treat the program output as classical.)
But your use (iiuc!) seems less radical. You are kind of just using linear logic as a way to specify a world model. But I don’t see what this does for you. What am I missing?
CDT and EDT have known problems on 5 and 10. TDT/UDT are insufficiently formalized, and seem like they might rely on known-to-be-unfomalizable logical counterfactuals.
So 5 and 10 isn’t trivial even without spurious counterfactuals.
What does this add over modal UDT?
No requirement to do infinite proof search
More elegant handling of multi-step decision problems
Also works on problems where the agent doesn’t know its source code (of course, this prevents logical dependencies due to source code from being taken into account)
Philosophically, it works as a nice derivation of similar conclusions to modal UDT. The modal UDT algorithm doesn’t by itself seem entirely
well-motivated; why would material implication be what to search for? On the other hand, every step in the linear logic derivation is quite natural, building action into the logic, and encoding facts about what the agent can be assured of upon taking different actions. This makes it easier to think clearly about what the solution says about counterfactuals, e.g. in a section of this post.
I haven’t tried as hard as I could have to understand, so, sorry if this comment is low quality.
But I currently don’t see the point of employing linear logic in the way you are doing it.
The appendix suggests that the solution to spurious counterfactuals here is the same as known ideas for resolving that problem. Which seems right to me. So solving spurious counterfactuals isn’t the novel aspect here.
But then I’m confused why you focus on 5&10 in the main body of the post, since that’s the main point of the 5&10 problem.
Maybe 5&10 is just a super simple example to illustrate things. But then, I don’t know what it is you are illustrating. What is linear logic doing for you that you could not do some other way?
I have heard the suggestion that linear logic should possibly be used to aid in the difficulties of logical counterfactuals, before. But (somehow) those suggestions seemed to be doing something more radical. Spurious counterfactuals were supposed to be blocked by something about the restrictive logic. By allowing the chosen action to be used only once (since it gets consumed when used), something nicer is supposed to happen, perhaps avoiding problematic self-referential chains of reasoning.
(As I see it at the moment, linear logic seems to—if anything—work against the kind of thing we typically want to achieve. If you can use “my program, when executed, outputs ‘one-box’” only once, you can’t re-use the result both within Omega’s thinking and within the physical choice of box. So linear logic would seem to make it hard to respect logical correlations. Of course this doesn’t happen for your proposal here, since you treat the program output as classical.)
But your use (iiuc!) seems less radical. You are kind of just using linear logic as a way to specify a world model. But I don’t see what this does for you. What am I missing?
CDT and EDT have known problems on 5 and 10. TDT/UDT are insufficiently formalized, and seem like they might rely on known-to-be-unfomalizable logical counterfactuals.
So 5 and 10 isn’t trivial even without spurious counterfactuals.
What does this add over modal UDT?
No requirement to do infinite proof search
More elegant handling of multi-step decision problems
Also works on problems where the agent doesn’t know its source code (of course, this prevents logical dependencies due to source code from being taken into account)
Philosophically, it works as a nice derivation of similar conclusions to modal UDT. The modal UDT algorithm doesn’t by itself seem entirely well-motivated; why would material implication be what to search for? On the other hand, every step in the linear logic derivation is quite natural, building action into the logic, and encoding facts about what the agent can be assured of upon taking different actions. This makes it easier to think clearly about what the solution says about counterfactuals, e.g. in a section of this post.