The post on naturalistic logical updates left open the question of whether the probability distribution converges as we condition on more logical information. Here, I show that this cannot always be the case: for any computable probability distribution with naturalistic logical updates, we can show it proofs in an order which will prevent convergence. In fact, at any time, we can drive the probability of $x$ up or down as much as we like, for a wide variety of sentences $x$.

As an aid to intuition, I describe the theorem informally as "all mathematicians are trollable". I was once told that there was an "all mathematicians go to Bayesian hell" theorem, based on the fact that a computable probability distribution must suffer arbitrarily large log-loss when trying to model mathematics. The idea here is similar. We are representing the belief state of a mathematician with a computable probability distribution, and trying to manipulate that belief state by proving carefully-selected theorems to the mathematician.

---

(ETA: A way around this result has now been found, giving us an untrollable mathematician.)

$\square p$ represents "p is provable", but we consider a class of proofs which the mathematician believes are sound; this justifies characterizing the mathematician's beliefs with the provability logic $GLS$ (as in naturalistic logical updates) rather than $GL$, so the mathematician's beliefs will obey the principle $\square p\to p$. For concreteness, we can suppose that the mathematician accepts proofs in $PA$.

Definition. A probability assignment over a language $L$ is a function from sentences of that language to values in the interval $[0,1]$.

This is, of course, an extremely weak definition. We will generally also want coherence with respect to some logic. Where a logic $A$ is a set of axioms and inference rules over $L$, we define coherence as usual:

Definition. A probability assignment $P$ over $L$ is coherent with respect to $A$ if and only if:

1. $⊢a$ implies $P\left(a\right)=1$ and $a⊢\perp$ implies $P\left(a\right)=0$,
2. whenever $a⊢b$, we have $P\left(a\right)\le P\left(b\right)$, and
3. $P\left(a\right)+P\left(b\right)=P(a\vee b)+P(a\wedge b)$.

This is equivalent to a number of other common definitions of coherence. For a computable probability assignment, coherence with $PA$ won't be possible. Requirement (1) alone is impossible: the sentences which can be proven from $PA$ and those which can be refuted are recursively inseparable sets.

We can, however, insist that the probability assignment is coherent with respect to $GLS$. To be more precise, we can translate all the axioms and inference rules of $GLS$ over to the language of $PA$ by interpreting the modal provability operator $\square$ as a provability predicate in $PA$. I will keep using the box-notation for simplicity, and will refer to $GLS$-derivability, $GLS$-coherence, and so on; I always mean it in this translated sense.^1^ Since the consequence relation of $GLS$ is decidable, we don't run into the same problem as we do for coherence with respect to $PA$; I showed previously that this allows a probability distribution to be constructed. In most respects, this is much weaker than coherence with respect to $PA$; however, it validates the soundness of proofs in $PA$, which $PA$ itself cannot.

The motivation for $GLS$-coherence in my previous post was reflective consistency: when a new mathematical fact is proven, we want to take it into account in a way which our past self would endorse. More precisely, I proposed that in the absence of interactions between impossible possible worlds (such as counterfactual mugging with a logical coin), the policy for responding to logical information which looks best before getting a proof one way or the other should still look like the best way of responding after a proof is found. I also argued something similar from logical Dutch Book arguments, though I hadn't found the $GLS$ recipe to satisfy the desiderata yet. These decision-theoretic arguments still needs to be dealt with in more detail, but it suggested to me the goal of making a computable probability assignment in which Bayesian updates on proofs take the place of the "second update" usually associated with logical uncertainty. The $GLS$-coherent prior which I constructed was the result.

In order for this approach to be very appealing, it seems that updating on proofs in this way should have other good properties which we have established for logical uncertainty, such as uniform coherence. The assignment which was given last time does not achieve such good properties, but perhaps some $GLS$-coherent probability assignment will. The major point of this post is to show a difficulty in achieving uniform coherence with such an approach: it is not possible for $GLS$-coherent Bayesian updates on proofs to have convergence guarantees when proofs are presented in arbitrary order. This does not rule out convergence for "good" proof orderings (indeed, perhaps there is a large class if "good" orderings for which we can converge); however, it is a bad sign. If convergence turns out to be impossible or very fragile, uniform coherence would as well.

Translating back to the story about "trolling mathematicians", the idea is to show that if someone is choosing proofs adversarially, a mathematician with $GLS$-coherent beliefs can be made to form arbitrarily strong conjectural beliefs for or against a target proposition $x$ (so long as this proposition has not yet been proved or disproved); these beliefs can be made to oscillate as desired. The adversary can do this without ever lying to the mathematician.

The initial idea of the proof is that because a computable probability assignment cannot be coherent with respect to $PA$, any statement $x$ has consequences in $PA$ which are currently unrecognized. Showing the mathematician a proof of those unexpected consequences should reduce belief in $x$, since it eliminates some of the ways $x$ could be true (removing $x$ as a possibility from situations where $\neg y$). (A real-life example of this is that learning about the Banach-Tarski paradox may reduce belief in the axiom of choice.) Furthermore, since learning $x\to y$ tends to decrease belief in $x$ and increase it in $y$, we can reduce the probability of a statement arbitrarily far by putting it as $x$ and finding many $y$ which it implies, or we can increase the probability of a statement by taking it to be $y$ and finding many $x$ which imply it.

The proof doesn't quite go through that simply, however; we will actually manipulate the probability of the statement $\neg \square \neg x$, rather than manipulating $x$ directly. $\neg \square \neg x$ is abbreviated as $◊x$. I also argue by choosing $y$ which is a theorem in $PA$, making $x\to y$ vacuously true; this simplifies the proof. Where $\neg x$ is a theorem, I will call $x$ and anti-theorem.

Lemma. Consider a computable probability assignment $P$ over the sentences of $PA$, such that $P$ is coherent with respect to $GLS$. For any $x$ such that $P\left(◊x\right)\ne 0$, there exists a theorem of $PA$, $y$, such that $P\left(◊y|◊x\right)\le 1/2$.

Proof. The expression $P\left(◊y|◊x\right)>1/2$ cannot act as a separator between $y$ which are theorems and anti-theorems of $PA$, since they are recursively inseparable. Due to $GLS$-coherence, and assuming $P\left(◊x\right)\ne 0$, there will already be some theorems of $PA$ for which this expression has value 1 and anti-theorems for which it is 0; for example, $P\left(◊\right(a\vee \neg a\left)|◊x\right)=1$ for any sentence $a$, and $P\left(◊\right(a\wedge \neg a\left)|◊x\right)=0$. Therefore, to prevent separation, there must be either an anti-theorem $c$ with $P\left(◊c|◊x\right)>1/2$, or a theorem $t$ with $P\left(◊t|◊y\right)\le 1/2$.

Suppose there's an anti-theorem $c$ with $P\left(◊c|◊x\right)>1/2$. Then $P\left(\neg ◊c|◊x\right)\le 1/2$. $\neg ◊c=\square \neg c$, and $\square \neg c$ implies $\neg \square c$ in $GLS$ (since $\neg \square \perp$ and also $\left(\right(\square c)\wedge (\square \neg c\left)\right)\to \square \perp$). $\neg \square x$ is $GLS$-equivalent to $◊\neg c$. By $GLS$-coherence, $P\left(◊\neg c|◊x\right)\le P\left(\neg ◊c|◊x\right)$. But this means that $\neg c$ is a $PA$-theorem with $P\left(◊\neg c|◊x\right)\le 1/2$.

Therefore, in either case, there is a $PA$-theorem $y$ such that $P\left(◊y|◊x\right)\le 1/2$. $■$

For the next theorem, I also need a condition which I will call weak non-dogmatism:

Defintion. A probability assignment on the language of $PA$ is weakly non-dogmatic if it does not assign probability zero to any theorem of $PA$.

The $GLS$-coherent prior which I constructed previously is weakly non-dogmatic; I take this to be a very reasonable requirement which is not at all difficult to meet.

Note that weak non-dogmatism together with $GLS$-coherence further implies that theorems of the combined system $PA+GLS$ have nonzero probability.

Theorem 1. For any computable probability assignment $P$ over the sentences of $PA$ which is $GLS$-coherent and weakly non-dogmatic, for any $x$ such that $1>P\left(◊x\right)>0$, there exists a theorem $t$ of $PA$ such that $P\left(◊x|\square t\right)/P\left(\neg ◊x|\square t\right)\le \frac{1}{2}P\left(◊x\right)/P\left(\neg ◊x\right)$; that is, odds of $◊x$ reduce by half given that $t$ is a theorem.

Proof. We will show this with the theorem $t=x\to y$, with $y$ chosen via the lemma. $x\to y$ is a theorem of $PA$, since $y$ is. So, we want to show $P\left(◊x|\square \right(x\to y\left)\right)/P\left(\neg ◊x|\square \right(x\to y\left)\right)\le \frac{1}{2}P\left(◊x\right)/P\left(\neg ◊x\right)$. The quantities are well-defined thanks to weak non-dogmatism and the assumption $1>P\left(◊x\right)>0$. Simplifying:

$\iff P(◊x\wedge \square (x\to y\left)\right)/P(\neg ◊x\wedge \square (x\to y\left)\right)\le \frac{1}{2}P\left(◊x\right)/P\left(\neg ◊x\right)$

$\iff P(◊x\wedge \square (x\to y\left)\right)/P\left(\neg ◊x\right)\le \frac{1}{2}P\left(◊x\right)/P\left(\neg ◊x\right)$ (The conjunct $\square (x\to y)$ in the divisor was redundant, since $\neg ◊x$ means $\square \neg x$, which already implies $\square (x\to z)$ for any $z$.)

$\iff P(◊x\wedge \square (x\to y\left)\right)\le \frac{1}{2}P\left(◊x\right)$

So, we want to show that $◊x\wedge \square (x\to y)$ is at most half as probable as $◊x$.

But we already know $P\left(◊y|◊x\right)\le \frac{1}{2}$, which means $P(◊y\wedge ◊x)\le \frac{1}{2}P\left(◊x\right)$. $(\neg \square \neg x\wedge \square (x\to y\left)\right)$ implies $\neg \square \neg y$, since if we could prove $\neg y$, we could combine that with a proof of $x\to y$ to prove $\neg x$. So by $GLS$ coherence, $P(◊x\wedge \square (x\to y\left)\right)\le P(◊y\wedge ◊x)$. So we have $P(◊x\wedge \square (x\to y\left)\right)\le \frac{1}{2}P\left(◊x\right)$, which is what was to be proved. $■$

This theorem allows us to cut the odds of $◊x$ in half (or more) by a set formula. Since the result of updating on $\square (x\to y)$ will itself be a $GLS$-coherent probability assignment (thanks in part to weak non-dogmatism), we can keep doing this, cutting the probability of $◊x$ down as much as we like.

Corollary 1. For $x$ such that $1>P\left(◊x\right)>0$, we can drive $P\left(x\right)$ as low as we like.

Proof. $GLS$ proves $\square \neg x\to \neg x$, so it also proves $x\to \neg \square \neg x$. Since $GLS$ has modus ponens as an inference rule, this means $x⊢◊x$, so $P\left(x\right)\le P\left(◊x\right)$. Since we can iterate the trick in Theorem 1 to drive down the probability of $◊x$ arbitrarily far, we can drive down $P\left(x\right)$ as well. $■$

Corollary 2. If we have $1>P\left(\square x\right)>0$, we can drive $P\left(x\right)$ as high as we like.

Proof. By corollary 1, we can drive $P\left(\neg x\right)$ down as far as we like in this case. $■$

The two corollaries identify cases when a "troll" can make a mathematician's belief arbitrarily low or high. The next theorem shows that we can combine the trick to send a mathematician's beliefs waver back and forth forever.

Theorem 2. Consider a sequence of weakly non-dogmatic $GLS$-coherent probability assignments $P_1,P_2,P_3,...$ such that $P_{n+1}$ is a Bayesian update of $P_n$ on some sentence $\square t$ with $t$ being a theorem of $PA$. We can insert additional updates on theorems, making a modified sequence $P_n^{\ast }$, to ensure that for some $x$, $P_n^{\ast }\left(x\right)$ does not converge to any value.

Proof. There must be undecidable sentences $u$ with both $P\left(\square u\right)>0$ and $P\left(\square \neg u\right)>0$. If there weren't, then all undecidable sentences would have either $P\left(\square x\right)=0$ or $P\left(\square \neg x\right)=0$. By weak non-dogmatism, theorems would have $P\left(\square x\right)>0$, and anti-theorems would have $P\left(\square \neg x\right)>0$. Sentences with both above zero would be guaranteed decidable one way or the other, so we could run a theorem prover and be sure that it would terminate on those. Sentences with both zero would be definitely undecidable. We can find the remaining theorems from anti-theorems by the predicate $P\left(\square x\right)>0\wedge P\left(\square \neg x\right)=0$. Thus, we have a procedure for deciding whether a given $x$ is a theorem or not in finite time, which is impossible.

Since $\square x$ implies $◊x$, we also have $P\left(◊u\right)>0$, which means $P\left(\square \neg u\right)<1$. Similarly, because $\square \neg x$ implies $◊\neg x$, we can infer $P\left(◊\neg u\right)>0$ and hence $P\left(\square u\right)<1$. So the sentences $u$ meet the conditions of corollaries 1 and 2.

Furthermore, there will be some sentences which stay in this state forever. If not, then it would be the case that we eventually know at least one of $\neg \square u$ or $\neg \square \neg u$ for these $u$. In fact, this means we eventually know one of those for any $x$ whatsoever. But this would allow us to separate theorems and anti-theorems: simply wait for one of $P\left(\square x\right)$ or $P\left(\square \neg x\right)$ to become zero, grouping the first case with anti-theorems and the second with theorems. This procedure would always halt, and never put a theorem in the anti-theorem group or vice versa. This can't happen, so there must be sentences whose state we stay uncertain about forever.

Therefore, we can cause a failure of convergence by driving the probability of these sentences up and down forever. Suppose, as in the theorem statement, that there is a sequence of weakly non-dogmatic $GLS$-coherent probability assignments $P_1,P_2,P_3,...$ such that $P_{n+1}$ is a Bayesian update of $P_n$ on some sentence $\square t$ with $t$ being a theorem of $PA$. Denote the sequence of theorems used as $t_1,t_2,t_3,...$. We can edit the sequence to be sure that there are sentences for which the probability assignment does not converge, as follows. Between $t_{2^n}$ and $t_{2^n+1}$ for whole-numbered $n$, insert additional theorems as follows. Find the first $n$ sentences matching the conditions of both corollaries 1 and 2. Use the strategy in corollary 1 to at least half the odds of these sentences $n$ times each, and then apply the strategy of corollary 2 to at least double them $n$ times each.

This guarantees that some sentences will have probability assignments which go back and forth forever, coming arbitrarily close to both probability 1 and probability 0 as the probability assignment is conditioned on more information. $■$

Are Naturalistic Updates to Blame?

I think some people might look at this and think that my unusual choice to update on $\square x$ rather than $x$ and to use the provability logic $GLS$ rather than the more usual $GL$ might be the source of the difficulty. However, updating on theorems $x$ directly rather than updating on their provability is just as bad (in fact a little worse). The following proof is due primarily to Scott Garrabrant (and was the seed idea for the proof of theorem 1):

Theorem 3. Consider a propositionally coherent probability assignment $P$ to the language of $PA$ which is computable and weakly non-dogmatic. For any sentence $x$ with $0<P\left(x\right)<1$, we can choose a sequence of theorems of $PA$ to update on which send $P\left(x\right)$ arbitrarily high or low.

Proof. There must be a theorem $t$ of $PA$ such that $P\left(t|x\right)\le \frac{1}{2}$, by the same seperability argument used in the proof of theorem 1. I want to establish that $P(a|a\to t)/P(\neg a|a\to t)\le \frac{1}{2}P\left(a\right)/P\left(\neg a\right)$. The expressions involved are well-defined thanks to weak non-dogmatism and the assumed range of $P\left(x\right)$. Reducing, it suffices to show:

$P(a\wedge (a\to t\left)\right)/P(\neg a\wedge (a\to t\left)\right)\le \frac{1}{2}P\left(a\right)/P\left(\neg a\right)$

Since $a\wedge (a\to t)$ is propositionally equivalent to $a\wedge t$, and $\neg a\wedge (a\to t)$ is propositionally equivalent to $\neg a$, so it suffices to show:

$P(a\wedge t)/P\left(\neg a\right)\le \frac{1}{2}P\left(a\right)/P\left(\neg a\right)$

$\iff P(a\wedge t)\le \frac{1}{2}P\left(a\right)$

But we already know $P\left(t|x\right)\le \frac{1}{2}$, which is to say $P(t\wedge x)\le \frac{1}{2}P\left(a\right)$.

This allows us to cut the odds of $x$ in half. A symmetric trick allows us to inflate the odds by half, using an anti-theorem $c$ and updating on $c\to x$. We can repeat both tricks as much as we like to drive the odds arbitrarily down or up. $■$

So it is not exactly the formalism of naturalistic updates which creates the central problem, but rather, has more to do with representing a belief-state as a computable probability assignment and perform a Bayesian update to take into account more information. On the other hand, the details (such as updating on $\square t$ rather than $t$) do change the prognosis somewhat (changing the conditions under which we can manipulate a sentence's probability); it might even be that there are mild variations which significantly improve things.

Discussion

I've shown that logical uncertainty following the school of naturalistic logical updates is "trollable", IE, can be manipulated by another entity selectively revealing mathematical proofs. This makes convergence (at best) dependent on proof order, which seems like a bad sign: logical uncertainty results so far haven't needed to make many assumptions about the theorem provers being used.

Although convergence/divergence is a nice formal property to check, one might argue that it doesn't matter too much what we believe about undecidable sentences. Decidable sentences will eventually be proved or refuted, and so will always converge. However, the proof also demonstrates that we can manipulate the probabilities of a large class of sentences, before those sentences are proved or refuted. This suggests that adversarial proof orderings can cause a $GLS$-agent to be arbitrarily wrong about sentences which are later proved/refuted.

The main concern is not so much whether $GLS$-coherent mathematicians are trollable as whether they are trolling themselves. Vulnerability to an external agent is somewhat concerning, but the existence of misleading proof-orderings brings up the question: are there principles we need to follow when deciding what proofs to look at next, to avoid misleading ourselves?

How damning is this for naturalistic logical updates, as a line of research? Speaking for myself, I find it concerning but not yet totally damning. The way I see it, this puts untrollability at odds with (a specific form of) reflective coherence: an agent shifting its mathematical uncertainty according to something other than a Bayesian update on proofs would want to self-modify, but an agent which uses a Bayesian update is more vulnerable to trolls. ("Trollability is bad, but if I can get a higher expected utility by editing myself to be more vulnerable to trolls, who cares?") I'm still somewhat hopeful that a probability assignment can converge on a broad class of proof-orderings. For example, it would be very nice if there were a $GLS$-coherent distribution which was not trollable by any proof-ordering within its own range of computational complexity ("successful trolls need more processing power than their targets"). I think a result like that is unlikely, at present, but I haven't ruled it out yet. We could then guarantee convergence by allocating more computational resources to the logical uncertainty than to the theorem prover (or, something resembling this).

One comment I got about this, in a discussion at MIRI (I forget who made the remark) was that it's a problem of updating on information without taking into account the source of the information. Just as you would draw different conclusions about the frequencies of colors in a ball pit if you knew someone was selecting balls at random to show you vs if you thought they were selecting by some other policy, you should be able to model the proof-selecting strategy of a troll; believing with high probability that they will be showing you more evidence against $x$, you would be inoculated against needing to actually adjust beliefs (unless the evidence was surprisingly compelling). I haven't figured out a good way to model this yet, though.

On the MIRIx slack, Miëtek Bak discussed explicit provability logic (papers: 1, 2). The idea is that reasoning about the existential statement "there exists a proof", in the form of "$\square$", causes unnecessary problems in reflection due to its non-constructive nature. Instead, we can consider a system which has explicit terms for proofs, with terms $p:s$ ("$p$ is a proof of $s$") taking the place of $\square s$. Like $GLS$, the resulting system can conclude the raw statement from the statement of provability; it endorses all instances of $(p:s)\to s$. Like $GL$, provability is reflective, representing provability in-this-very-logic. This may make explicit provability a good candidate for a variant of naturalistic logical updates. I think there may be reflective consistency considerations which point in this direction as well: my argument for naturalistic logical updates involves the agent considering the future, but makes a perhaps problematic leap from the agent observing a proof to the agent observing abstract provability, "$\square$". (This is especially questionable given that the agent is not supposed to be making first-order inferences like that automatically.)

Overall, naturalistic logical updates stand or fall with the strength of the reflective consistency argument which I'm currently claiming leads us to them. I haven't articulated this well enough yet, I think. (But, see logical Dutch Book arguments, logical counterfactuals consistent under self-modification, and naturalistic logical updates for my arguments as they stand.)

---

1. This still leaves details to the imagination, so to be yet more precise: consider a (computable) encoding of sentences $s$ of the language of $PA$ into numerals $┌s┐$, and another encoding $└p┘$ of proofs $p$ of $PA$ as numerals. There exists a predicate in $PA$ which checks whether $p$ is a proof of $s$; denote it as $Proves(└p┘,┌s┐)$. Also, we will use a function $f\left(\right)$ giving unique propositional sentence-letters of $GLS$ for each expression of $PA$; this function must have the property that syntactically distinct expressions always get distinct propositional sentence-letters (no "hash collisions"), while identical expressions are given the same sentence-letter. We encode statements from $PA$ into $GLS$ by a recursive translation $Tr\left(\right)$:

• $Tr\left[\neg a\right]=\neg Tr\left[a\right]$
• $Tr[a\wedge b]=Tr\left[a\right]\wedge Tr\left[b\right]$
• $Tr[a\vee b]=Tr\left[a\right]\vee Tr\left[b\right]$
• $Tr[\exists x.Proves(x,┌a┐\left)\right]=\square Tr\left[a\right]$
• Otherwise, $Tr\left[a\right]=f\left(a\right)$

The abuse of language whereby I talk about consequence and coherence "in $GLS$", but concerning the sentences of $PA$, can now be justified by translating $PA$ sentences into $GLS$ to check the consequence relation. Notice that since identical sub-expressions always get translated to the same sentence-letters in $GLS$, we can validate $GLS$ principles like $a\vee \neg a$ and $a⊢a$ for all sentences $a$ in $PA$; however, we make quantifiers totally opaque, failing to recognize even simple equivalences such as $(\forall x.x=x)\leftrightarrow (\forall y.y=y)$.