Nice. I think this maps more precisely in the case where you ask questions about yourself. In this case, you can (in some cases) be assured that you will find no proof about what action you will take, but you can still prove things about logical consequences of your action. So the difference between the “shorter” proof and the “longer” proof is that you can’t actually find the longer proof.
My intuition about logical counterfactuals in general is that it seems easier to just solve agent-simulates-predictor type problems directly than to solve logical counterfactuals, since at least there’s a kind of win condition for ASP-type problems. So the statements about proof length here might map to facts about whether a bounded predictor can predict things about you. In ASP we want “Bounded predictor predicts that agent do X” to be considered a logical counterfactual of “agent does X” from the agent’s perspective; this would require there to be a short proof of “agent does X → bounded predictor predicts agent does X”. But we don’t get this automatically: this would require the agent to use a reasoning system that the predictor can reason about somehow. I might write another post on intuitions about ASP-type problems.
Nice. I think this maps more precisely in the case where you ask questions about yourself. In this case, you can (in some cases) be assured that you will find no proof about what action you will take, but you can still prove things about logical consequences of your action. So the difference between the “shorter” proof and the “longer” proof is that you can’t actually find the longer proof.
My intuition about logical counterfactuals in general is that it seems easier to just solve agent-simulates-predictor type problems directly than to solve logical counterfactuals, since at least there’s a kind of win condition for ASP-type problems. So the statements about proof length here might map to facts about whether a bounded predictor can predict things about you. In ASP we want “Bounded predictor predicts that agent do X” to be considered a logical counterfactual of “agent does X” from the agent’s perspective; this would require there to be a short proof of “agent does X → bounded predictor predicts agent does X”. But we don’t get this automatically: this would require the agent to use a reasoning system that the predictor can reason about somehow. I might write another post on intuitions about ASP-type problems.