Update: This version of the Trolljecture fails too; see the counterexample due to Sam.

In An Informal Conjecture on Proof Length and Logical Counterfactuals, Scott discussed a "trolljecture" from a MIRI workshop, which attempted to justify (some) logical counterfactuals based on the lengths of proofs of various implications. Then Sam produced a counterexample, and Benja pointed to another counterexample.

But at the most recent MIRI workshop, I talked with Jonathan Lee and Holger Dell about a related way of evaluating logical counterfactuals, and we came away with a revived trolljecture!

---

Let's say we have a recursively enumerable set of axioms $S$ (in the language of PA) and a statement $\phi$. Then we define the "distance" $d_S\left(\phi \right)$ as the length of the shortest proof of $\phi$ using the axioms $S$. (We set $d_S\left(\phi \right)=\infty$ if there is no such proof.)

And now we define a valuation $${\nu }_S\left(\phi \right)=\frac{d_S\left(\neg \phi \right)}{d_S\left(\neg \phi \right)+d_S\left(\phi \right)}$$ which we will interpret as the "probability" of the logical counterfactual that $S$ implies $\phi$. (This is undefined when $\phi$ is undecidable given $S$; we could define it as a limit when searching over proofs of bounded length, in which case it would equal 0.5 in such cases. But as we shall see, this is not the case we care about.)

This valuation has the trivial properties that ${\nu }_S\left(\phi \right)=1$ if $S⊢\phi$ and $S⊬\neg \phi$, and similarly ${\nu }_S\left(\phi \right)=0$ if $S⊬\phi$ and $S⊢\neg \phi$. But what's more interesting are the properties that this valuation has if $S$ is inconsistent.

If there is a short proof of $\phi$ from $S$, and a much longer proof of $\neg \phi$ from $S$, then ${\nu }_S\left(\phi \right)\approx 1$. Moreover, we have an approximate coherence condition $${\nu }_S(\phi \wedge \psi )+{\nu }_S(\phi \wedge \neg \psi )\approx {\nu }_S\left(\phi \right)$$ so long as either $\phi$ or $\psi$ has a proof from $S$ that is much shorter than the proof of $\perp$ from $S$. (See the notes below.)

And this gets some key examples "correct" if we add the axioms that we actually care about (and which make the problem truly counterfactual). For instance, let's take Sam's counterexample to the original Trolljecture:

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

def A():
  if PA ⊢ A() = 1 → U() = 10:
    return 1
  else: return 2

In that case, $A\left(\right)$ actually returns 2 and $U\left(\right)$ returns 5, but PA proves the "incorrect" counterfactual that $A\left(\right)=1\to U\left(\right)=0$ and does not prove the "correct" counterfactual that $A\left(\right)=1\to U\left(\right)=10$. (Read the linked post if this puzzles you.)

But what if we consider reasoning from the inconsistent premises that PA is consistent and yet $A\left(\right)=10$? In that case, I claim that ${\nu }_{\text{PA+Con(PA)}+\left(A\right()=1)}\left(U\right()=10)$ is near 1 while ${\nu }_{\text{PA+Con(PA)}+\left(A\right()=1)}\left(U\right()=0)$ is near 0.

To see this, note that there is a short proof from these axioms that $U\left(\right)=10$ (look at the definition of $U$, apply the axiom that $A\left(\right)=1$, apply the axiom $\text{Con(PA)}$, and conclude that $U\left(\right)=10$), but the shortest proof from those axioms that $U\left(\right)=0$ is longer: we would need to prove Godel's Second Incompleteness Theorem to show that $\text{Con(PA)}\to A\left(\right)=2$, thus $\neg \text{Con(PA)}$, and thus $U\left(\right)=0$.

(Of course, I could be missing a much shorter proof, but I think this particular example goes through. The same reasoning also holds for the example Benja mentioned.)

Therefore, I will go out on a limb and propose the following:

Revived Trolljecture: If we consider a modal agent $A\left(\right)$ inside a modal universe $U\left(\right)$, then for sufficiently large $N$, the "correct" logical counterfactuals of the form "if $A\left(\right)=a$, then $U\left(\right)=u$" are the ones such that the valuations ${\nu }_{\text{PA+N}+\left(A\right()=a)}\left(U\right()=u)$ are high. In particular, if for $N$ sufficiently large, there is a short proof in $\text{PA+N}$ of $A\left(\right)=a\to U\left(\right)=u$ and no comparably short proof of $A\left(\right)\ne a$, then $u$ is unique with this property, and this is the "correct" counterfactual utility for $A\left(\right)=a$.

I'm not very confident that this is true as stated, but I have some reasonable hope that either a counterexample will be enlightening about logical counterfactuals, or that an improved analogue of the valuation will in fact be quite useful.

Notes on this valuation:

• This is a claim about "third person" counterfactuals, not those done by an agent itself. Obviously, an agent that makes decisions based on this valuation will not be definable in modal logic, and I don't yet make any claims about what such an agent might do in the PA versions of such problems.

• The approximate coherence is of the following form: if the shortest proof of contradiction from $S$ has length $N$, and one of the statements $\phi$, $\neg \phi$, $\psi$, $\neg \psi$ has a proof from $S$ of length $n\ll N$, then $${\nu }_S(\phi \wedge \psi )+{\nu }_S(\phi \wedge \neg \psi )={\nu }_S\left(\phi \right)+O\left(n/N\right).$$ I don't know a cleverer proof than going through the cases, but each case is straightforward. For instance, if $d_S\left(\phi \right)=n$, then we must have $N-n\le d_S\left(\neg \phi \right)\le N+1$, and so it follows quickly that ${\nu }_S\left(\phi \right)=1+O\left(n/N\right)$; then, considering the three cases $d_S\left(\psi \right)\lesssim n$, $d_S\left(\neg \psi \right)\lesssim n$, and neither, in each case it is clear that ${\nu }_S(\phi \wedge \psi )={\nu }_S\left(\psi \right)+O\left(n/N\right)$.

• It does not, however, seem to be the case that ${\nu }_S(\phi \wedge \psi )+{\nu }_S(\phi \wedge \neg \psi )\approx {\nu }_S\left(\phi \right)$ whenever there is an easily provable relation between $\phi$ and $\psi$. I am not entirely sure that I'm not missing a necessary logical relation, but it seems like we could consider two sentences $\phi$ and $\theta$ whose proofs are "independent" of the contradiction in $S$ and of each other, and then let $\psi =\phi \wedge \theta$ so that $\psi \to \phi$ is quickly provable from $S$. Say that $d_S\left(\perp \right)=N$, $d_S\left(\phi \right)=N/2$, $d_S\left(\theta \right)=N/3$; if these are independent in that way, we should be able to get $d_S\left(\neg \phi \right)\approx N$, $d_S\left(\neg \theta \right)\approx N$, $d_S\left(\psi \right)\approx d_S\left(\phi \right)+d_S\left(\theta \right)\approx 5N/6$, and $d_S\left(\neg \psi \right)\approx N$. Then ${\nu }_S\left(\phi \right)\approx 2/3$, ${\nu }_S(\phi \wedge \psi )\approx {\nu }_S\left(\psi \right)\approx 6/11$, and ${\nu }_S(\phi \wedge \neg \psi )$ will be at least 1/4 since $d_S(\phi \wedge \neg \psi )\approx N$ and $d_S(\neg \phi \vee \psi )\ge N/3$, so ${\nu }_S(\phi \wedge \psi )+{\nu }_S(\phi \wedge \neg \psi )-{\nu }_S\left(\phi \right)>6/11+1/4-2/3>0$. I don't know whether this could be used to break the revived trolljecture.

• If the shortest proof of contradiction from $S$ has length $N$, then for any $\phi$, $\frac{1}{N+2}\le {\nu }_S\left(\phi \right)\le \frac{N+1}{N+2}$; the valuations are bounded away from 0 and 1. This may be a feature and not a bug: a mathematician could reason decently confidently about what math would look like in the counterfactual where Fermat's Last Theorem were false (presuming that its actual proof is quite long), but it is hard to say very much about what math would look like in the counterfactual where $1+1=3$. However, there are some examples, like naive set theory before Russell's Paradox, where human mathematicians reasoned mostly coherently despite using axioms that (they did not notice) led quickly to contradictions; the valuation does not capture that aspect of mathematical intuition.

• I restricted the new trolljecture to modal universes because it is well-specified how the stronger axiom schemas $PA+N$ eventually decide the agent and the universe in the standard model of the natural numbers. If something like it holds up here, then there may be a more general version.