In the first part, I explained that the two-update problem can be understood in two different ways: (1) adding an axiom $\varphi$ to a logic before defining a probability distribution $P$ for it is generally different from a Bayesian update on $\varphi$, and (2) improving our approximation of $P$ upon observing a proof of $\varphi$ is generally different from a Bayesian update. (These two forms appear to really be the same problem.)

This may not be fundamentally concerning: perhaps neither of these should be a Bayesian update. However, Paul Christiano's paradox of ignorance suggests that we will have some problems if we depart from Bayesian updates. I closed with the question of whether we can circumvent this by making the update-on-proofs into a Bayesian update; I'll address that question here.

What we would want to do is start with a probability distribution which is ignorant of logic, and do a Bayesian update on facts of logic as we prove them. (I think this suggestion was made once or twice elsewhere; I'll link to original sources as I find them, but let me know if you know of them.) Can this be made to work?

The simplest case is that we start out by assigning every statement a probability of 1/2, independent of all other statements. We then run our theorem-prover, and update on any proofs we find. This doesn't just mean updating single sentences as they are proved; indeed, this would do nothing to alter the probability of other sentences. The important thing is to eliminate combinations of sentence truth-assignments which are proven to be inconsistent. For example, if we find that $\varphi ⊢\psi$, we rule out the states where $\varphi$ is true and $\psi$ is false. If $\psi$ is a new sentence not yet touched by anything else, this modifies $P\left(\varphi \right)$ by a likelihood ratio of 1:2 (making it less probable since its truth depends on a more constrained circumstance). Similarly, if $\varphi$ is new, $P\left(\psi \right)$ is modified by the likelihood ratio 2:1.

It follows that no matter how far along in the process we are, the likelihood ratio of $\varphi$ is always being doubled or halved: it's halved when we encounter a proof of a new instance of $\varphi ⊢\varphi \vee \psi$ (choosing $\psi$ to select an untouched $\varphi \vee \psi$), and doubled when we encounter a new instance of $\varphi \wedge \psi ⊢\varphi$ (again, chosen so that $\varphi \wedge \psi$ is fresh). This means that the distribution can only converge if it converges to probabilities that are just 0 or 1. Furthermore, if $\varphi$ is never proved or disproved, whether it converges to 0 or 1 could be manipulated by changing the order of the proof search; we can bias search toward cases of $\varphi ⊢\varphi \vee \psi$ or of $\varphi \wedge \psi ⊢\varphi$ depending on which direction we want to drive $\varphi$.

(Again, I seem to recall that something like this has been discussed before -- let me know if you know where I should be linking to.)

So, this isn't any good. It seems like our initial distribution over sentences was too simplistic. For fixed $\varphi$, as we observe more and more proofs of $\varphi ⊢\psi$ or $\psi ⊢\varphi$, the probability of $\varphi$ should change less and less.

What if we start with the Solomonoff distribution over sentence truth-values, instead? We could regard a sequence of 0s and 1s as representing the truth and falsehood of sentences, with the $n$th position in the sequence telling us about the $n$th sentence. Unfortunately, logically consistent assignments of 1s and 0s are, taken together, an event of measure 0 in the Solomonoff distribution. There is no stochastic Turing machine which is guaranteed to produce such an assignment. (If there were such a machine, we could use it to specify a complete and consistent extension of $PA$ by feeding it 1s rather than random bits, and taking just the first-order statements of the form "the axioms of PA $\to$ ...".) This means the result of a Bayesian update is not defined by Bayes' theorem; perhaps we can construct something reasonable by taking limits, but this seems likely to run into the same problem as we saw with the prior which assigns 1/2 to everything.

Benja suggested a way to get around this: use a modified version of Solomonoff induction which uses Turing machines with a halting oracle. These machines can decide logical implication, and therefore will generate consistent assignments with nonzero probability.

Unfortunately, this approach will not be approximable. Machines with a halting oracle are equivalent to Schmidhuber's GTMs, which are not approximable for reasons exactly analogous to the halting problem.

What Benja effectively did is to say: let's use a mixture of all approximable probability distributions! This includes any reasonable probability distribution over logic we might ever come up with (if "reasonable" includes approximability). Updating on logic as a constraint is then straightforward. Sadly, this distribution is not itself approximable.

In the next post in this series, I plan to describe ways we considered to try and get around this.