An Informal Conjecture on Proof Length and Logical Counterfactuals

I (just yesterday) found a counterexample to this. The universe is a 5-and-10 variant that uses the unprovability of consistency:

def U():
  if A() == 2:
    if PA is consistent:
      return 10
    else:
      return 0
  else:
    return 5

The agent can be taken to be modal UDT, using PA as its theory. (The example will still work for other theories extending PA, we just need the universe's theory to include the agents. Also, to simplify some later arguments we suppose that the agent uses the chicken rule, and that it checks action 1 first, then action 2.) Since the agent cannot prove the consistency of its theory, it will not be able to prove $A\left(\right)=2\to U\left(\right)=10$, so the first implication which it can prove is $A\left(\right)=1\to U\left(\right)=5$. Thus, it will end up taking action 1.

Now, we work in PA and try to show $A\left(\right)=2\to U\left(\right)=0$. If PA is inconsistent (we have to account for this case since we are working in PA), then $A\left(\right)=2\to U\left(\right)=0$ follows straightforwardly. Next, we consider the case that PA is consistent and work through the agent's decision. PA can't prove $A\left(\right)\ne 1$, since we used the chicken rule, so since the sentence $A\left(\right)=1\to U\left(\right)=5$ is easily provable, the sentence $A\left(\right)=1\to U\left(\right)=10$ (ie. the first sentence that the agents checks for proofs of) must be unprovable.

The next sentence we check is $A\left(\right)=2\to U\left(\right)=10$. If the agent finds a proof of this, then it takes action 2. Otherwise, it moves on to the sentence $A\left(\right)=1\to U\left(\right)=5$, which is easily provable as mentioned above, and it takes action 1. Hence, the agent takes action 2 iff it can prove $A\left(\right)=2\to U\left(\right)=10$, so $$A\left(\right)=2\leftrightarrow \square (A\left(\right)=2\to U\left(\right)=10).$$ Löb's theorem tells us that $$\square \left(U=10\right)\leftrightarrow \square \left(\square \right(U=10)\to U\left(\right)=10),$$ so, by the uniqueness of fixed points, it follows that $A\left(\right)=2\leftrightarrow \square \left(U=10\right)$. Then, we get $A\left(\right)=2\to \square \left(U=10\right)$, so $A\left(\right)=2\to \square \left(\neg \square \perp \right)$ by the definition of the universe, and so $A\left(\right)=2\to \square \left(\perp \right)$ by Gödel's second incompleteness theorem. Thus, if the agent takes action 2, then PA is inconsistent, so $U\left(\right)=0$ as desired.

This tells us that $PA⊢A\left(\right)=2\to U\left(\right)=0$. Also, $PA⊬A\left(\right)\ne 2$ by the chicken rule, so $PA⊬A\left(\right)=2\to U\left(\right)\ne 0$. Since PA does not prove $A\left(\right)=2\to U\left(\right)\ne 0$ at all, the shortest proof of $PA⊢A\left(\right)=2\to U\left(\right)=0$ is much shorter than the shortest proof of $A\left(\right)=2\to U\left(\right)\ne 0$ for any definition of "much shorter". (One can object here that there is no shortest proof, but (a) it seems natural to define the "length of the shortest proof" to be infinite if there is no proof, and (b) it is probably straightforward but tedious to modify the agent and universe so that there is a proof of $A\left(\right)=2\to U\left(\right)\ne 0$, but it is very long.)

However, it is clear that $U\left(\right)=0$ is not a legitimate counterfactual consequence of $A\left(\right)=2$. Informally, if the agent chose action 2, it would have received utility 10, since PA is consistent. Thus, we have a counterexample.

One issue we discussed during the workshop is whether counterfactuals should be defined with respect to a state of knowledge. We may want to say here that we, who know a lot, are in a state of knowledge with respect to which $A\left(\right)=2$ would counterfactually result in $U\left(\right)=10$, but that someone who reasons in PA is in a state of knowledge w.r.t. which it would result in $U\left(\right)=0$. One way to think about this is that we know that PA is obviously consistent, irrespective of how the agent acts, whereas PA does not know that it is consistent, allowing an agent using PA to think of itself as counterfactually controlling PA's consistency. Indeed, this is roughly how the argument above proceeds.

I'm not sure that this is a good way of thinking about this though. The agents goes through some weird steps, most notably a rather opaque application of the fixed point theorem, so I don't have a good feel for why it is reasoning this way. I want to unwrap that argument before I can say whether it's doing something that, on an intuitive level constitutes legitimate counterfactual reasoning.

More worryingly, the perspective of counterfactuals as being defined w.r.t. states of knowledge seems to be at odds with PA believing a wrong counterfactual here. It would make sense for PA not to have enough information to make any statement about the counterfactual consequences of $A\left(\right)=2$, but that's not what's happening if we think of PA's counterfactuals as obeying this conjecture; instead, PA postulates a causal mechanism by which the agent controls the consistency of PA, which we didn't expect to be there at all. Maybe it would all make sense if I had a deeper understanding of the proof I gave, but right now it is very odd.

(This is rather long; perhaps it should be a post? Would anyone prefer that I clean up a few things and make this a post? I'll also expand on the issue I mention at the end when I have more time to think about it.)

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.

Neat. Okay, here's my sketch of a counterexample (or more precisely, a way in which this may violate my imagined desiderata for counterfactuals). A statement $\varphi$ that leads to a to a short proof of $\perp$ does not seem like the counterfactual ancestor of every single statement $\psi$ that does not lead to a short proof of $\perp$.

E.g. "5263=3126" doesn't seem like it counterfactually implies that there exists a division of the plane that requires at least 5 colors to fill in without having identical colors touch. It seem much more like it counterfactually implies "5163=3063" (i.e. the converse of the trolljecture seems really false).

But I dunno, maybe that's just my aesthetics about proofs that go through $\perp$. Presumably "legitimate counterfactual consequence" could be cashed out as some sort of pragmatic statement about a decision-making algorithm?