Vadim pointed out in a comment to my post on logical counterfactuals that a very similar idea had been explained in a LessWrong post summarizing work by Vladimir Slepnev and Paul Christiano at a MIRI workshop in 2013. The algorithm which they suggested was called UDT 1.5. In fact, the essential idea is already argued by Vladimir Slepnev (cousin_it) in a post from 2012: Should logical probabilities be updateless too?.

Here, I continue to develop these ideas and those in my logical dutch-book post. I present an alternate prior to the one which was used for UDT 1.5. I show that this new prior has naturalistic logical updates, a kind of improvement-endorsing property which seems likely to work well with UDT. This property also gets around Paul Christiano's paradox of ignorance.

---

Motivation

Slepnev motivates the problem with a variant of counterfactual mugging, inspired by a post by Wei Dai but simplified:

Suppose Omega (the near-omniscient near-omnipotent and almost perfectly trustworthy agent who prefers the pronouns ve/ver) appears before you. Omega tells you that ve has computed the millionth binary digit of $\pi$, and that before knowing what the digit was, ve had committed to the following procedure: if the millionth digit is zero, ask you for $100. If the millionth digit is one, give you $10,000 only if you would have given Omega the $100 had the digit been zero; otherwise, give you nothing. Omega then tells you that the millionth digit was in fact zero, and asks you for $100.

Suppose you already use a variant of UDT, so you take the actions you would have approved of ahead of time. If you are a "smart" agent who already knew the millionth digit of $\pi$ and only calculated expected utility of universes consistent with this knowledge, you'd turn Omega down. If you're a "dumb" agent who doesn't, you'd give Omega the $100. (This is true even though UDT uses a kind of logical counterfactual; a UDT agent takes a counterfactual on its possible actions, not anything else, so it still doesn't consider the worlds where digits of $\pi$ are different.)

This means that "dumb" agents don't want to become "smart" agents. A UDT-like agent which improves its beliefs over time by proving more theorems will be temporally inconsistent. This calls into question approaches to logical uncertainty which rely on estimates which improve given more time, such as uniform coherence.

My intuition is that we want to bite the bullet and be updateless about logical uncertainty as well as empirical uncertainty, because this maximizes expected value from a logically uncertain perspective. This makes it seem like the only reflectively consistent possibility. Scott Garrabrant gave me a different argument for the same conclusion. My recollection of the argument is as follows:

Problems like this are a result of someone simulating you. You can't be sure of whether you're in the simulation, being fooled into thinking the millionth digit of $\pi$ is zero, or whether you're in the real world. You can't trust your own logic, since it could be spoofed. If you're in the real world, you want to not give up the $100. If you're in the simulation, then you'd like to give it up so that the real you gets $10,000. However, as in the absentminded driver problem, the sleeping beauty problem, and other such problems, you shouldn't solve the problem by assigning probabilities to the two possibilities; instead, you want to act according to a policy you'd endorse ahead of time. Hence, an updateless solution.

(An interesting question: to what extent do the details of Omega's counterfactual computation determine whether we buy the whole argument?)

Naturalistic Logical Updates

It seems we need a logically ignorant prior which is used to judge policies. This is a prior over impossible possible worlds, so it is bound to include some nonsense, but it can't be as simple as assigning probability 1/2 to everything; there needs to be enough structure to get "reasonable" results. Slepnev and Christiano offered such a prior in the workshop results I mentioned, but I don't see that it gets me the properties I want. I will construct one according to the properties I see as desirable, along the lines I started to develop in my logical dutch book post.

A logically updateless UDT should reduce to a logically updateful DT in circumstances which do not involve entanglements with impossible possible worlds. I won't get that property here, but I will go for something suggestive: an approximation scheme for a logical prior which "endorses" improved approximations as being the appropriate update.

An AI which improves its logical consistency over time can be modeled by a sequence of approximate probability distributions $P_1\left(\varphi \right),P_2\left(\varphi \right),P_3\left(\varphi \right)...$ which are supposed to get better and better. For this post, the probability distribution will be over sentences of $PA$. I make the assumption that the change between any $P_n$ and $P_{n+1}$ in this sequence is due purely to information coming from a theorem-prover; at time $n+1$, we've proved more theorems, and taken them into account as logical constraints on beliefs. The type of constraints I will use will be partitions of truth: a set of sentences of which exactly one can be true. Coherence relative to a single constraint is defined by probabilities summing to one:

Relative Coherence: Where $\sigma$ is a finite set of sentences, $P\left(\varphi \right)$ is coherent relative to $\sigma$ if and only if ${\Sigma }_{\varphi \in \sigma }P\left(\varphi \right)=1$.

If a function is coherent relative to all provable partitions of truth, it is coherent in the standard sense. So, we can suppose that this is the only type of information which the theorem-prover gives us. (This is a version of coherence which I got from Scott.)

As I found when working on the logical Dutch book post, the behavior of conditional probabilities gets tricky when we only have relative coherence; we don't necessarily have basic properties of conjunction, so we can have things like $P\left(\varphi |\varphi \right)\ne 1$ and probabilities which depend on the order in which we condition on evidence. This is a problem for getting nice properties out of such probability functions. To solve this, I will require propositional coherence: the distribution will be coherent relative to every constraint which is provable by propositional logic alone. (Although this introduces an infinite number of constraints, $P_n\left(\varphi \right)$ can still be computable, as I will show later.) This is probably overkill, but is convenient.

Let $┌\sigma ┐$ be the sentence asserting that $\sigma$ is a partition of truth. (For example, if $\sigma =\left\{\varphi \right\}$, then $┌\sigma ┐=\varphi$; on the other hand, if $\sigma =\{\varphi ,\psi ,\theta \}$, then $┌\sigma ┐=(\varphi \vee \psi \vee \theta )\wedge \neg (\varphi \wedge \psi )\wedge \neg (\varphi \wedge \theta )\wedge \neg (\psi \wedge \theta )$.) We define a naturalistic update as follows:

Naturalistic Logical Update: $P\left(\varphi \right)$ has a naturalistic logical update if and only if:

• Where $\sigma$ is a partition of truth, $P(\varphi |\square ┌\sigma ┐)$ is coherent relative to $\sigma$.

This is the successor to my notion of "information-adding coherence" in the logical dutch book post. Note that this definition only requires coherence relative to real logical constraints. If $\sigma$ is not a genuine partition of truth, $P(\varphi |{\square }_n┌\sigma ┐)$ may or may not be coherent relative to $\sigma$. This is because coherence conditioning on arbitrary constraints would be impossible: we could condition on an unsatisfiable set of constraints.

We could then define $P_n\left(\varphi \right)$ by updating sequentially on theorems as we prove them. This won't be quite what's wanted, but it will give enough intuition for now. I'll use $C_n$ to denote the set of constraints $P_n\left(\varphi \right)$ has updated on.

For an updateless decision theory which uses $P_0\left(\varphi \right)$ as a logically ignorant prior, this means the segment of expected utility of a policy coming from just those worlds in which constraints $C_n$ are provable should be exactly the expected utility under $P_n\left(\varphi \right)$. If this possible world is sufficiently "isolated" from everything else (negligible probability of being simulated), then the preferred policy for this case should be very close to the policy for a logically updateful agent using $P_n\left(\varphi \right)$. This suggests there's some hope for a well-behaved UDT based on $P_0\left(\varphi \right)$.

This is "naturalistic" in the sense that it doesn't care where the proof comes from. The only difference between the internal theorem-prover and an external one is that the agent has perfect knowledge of it. If we instead update on observations which make it very probable that a external theorem-prover has proved something, the resulting distribution would be (almost) coherent with respect to those constraints. Note that this solves Paul Christiano's paradox of ignorance: the counterintiutive effect was precisely that updating on information from an external theorem-prover was different from updating on an internal one. (Christiano 2014, section 6.1.5.)

This level of self-trust might appear concerning for Lobian reasons. We can apply the naturalistic update property to prove $P\left(\varphi |\square \varphi \right)=1$; since $P\left(\varphi |\square \varphi \right)=P(\varphi \wedge \square \varphi )/P\left(\square \varphi \right)$, we have $P(\varphi \wedge \square \varphi )=P\left(\square \varphi \right)$; then $P(\square \varphi \wedge \neg \varphi )=0$; so we have $P(\square \varphi \to \varphi )=1$. However, recall that the naturalistic update property only applied to genuine partitions of truth; this line of argument only applies if $\varphi$ is a theorem in the first place. Furthermore, even if we construct a prior for which $P(\square \varphi \to \varphi )=1$ for a much wider class of $\varphi$ than only theorems, this would still be a far cry from having $\square (\square \varphi \to \varphi )$ in the proof system itself.

It turns out such a distribution can be constructed by surprisingly simple means.

Theorem. There exists a computable probability distribution $P^{\ast }\left(\varphi \right)$ which is coherent with respect to propositional constraints, and which has a naturalistic logical update.

Proof. Sample a random infinite theory $T^{\ast }$ as follows. Let $\mu \left(\varphi \right)$ be a positive probability distribution over sentences. Sampling from $\mu \left(\varphi \right)$ repeatedly, accept those samples into $T^{\ast }$ which are consistent with everything accepted so far under the provability logic $GLS$. (When I say a set of sentences is consistent under $GLS$, I mean the following: Take the conjunction of all the sentences. Translate this sentence to modal logic, hiding all details which aren't either propositional logic or the provability predicate. If the negation of the result is a theorem of $GLS$, the set of sentences is said to be inconsistent; otherwise, it is consistent.)

Define $P^{\ast }\left(\psi \right)$ as the probability that $\psi$ will occur in such a $T^{\ast }$. This is computable, as follows. Generate the tree of possible random theories, ending in a leaf whenever $\psi$ or $\neg \psi$ is sampled. The probability that one of the two will eventually be added to $T^{\ast }$ is 1, because $GLS$ extends propositional logic and so has the property that if both $\alpha \wedge \psi$ and $\alpha \wedge \neg \psi$ are inconsistent, $\alpha$ is already inconsistent. Therefore, for any desired accuracy $\epsilon >0$, we can extend the tree far enough to compute $P^{\ast }\left(\psi \right)$ to within $\epsilon$.

Suppose that $\sigma$ is a partition of truth which is provable by propositional means alone. Since $GLS$ extends propositional logic, any $T\ast$ sampled would contain at most one $\varphi \in \sigma$ to avoid inconsistency. Furthermore, since any $T^{\ast }$ eventually contains either $\varphi$ or $\neg \varphi$ for each $\varphi$, it will also contain at least one: otherwise, it would contain the negation of all sentences in $\sigma$, which would also be an inconsistency. Therefore, the probability of any propositional partition of truth sums to one, as required.

$P^{\ast }\left(\varphi \right)$ also has a naturalistic update. $GLS$ has $\square \varphi \to \varphi$ for all $\varphi$. Therefore, $P^{\ast }(\varphi |\square ┌\sigma ┐)$ is coherent relative to constraint $\sigma$. $\square$

It might seem strange that I've used $GLS$ rather than $GL$. $GLS$ is the "truth provability logic", which gives every true modal statement about provability in $PA$, rather those provable in $PA$. (Boolos, 1995.) $GL$ represents the knowledge about provability possessed by $PA$, whereas $GLS$ represents knowledge beyond $PA$. For example, $GLS$ proves $\neg \square \perp$. It might seem odd to impose this level of knowledge about provability on the probability distribution. However, coherence relative to $GL$ would be odd in other ways. $GL$ obeys "necessitation": $\varphi \to \square \varphi$. This means that anything true must be provable. This seems wrong for our logical prior: we're sampling random sentences to create a probability distribution in part because we know not everything is provable or disprovable, but want to have beliefs about those things anyway. Consistency with respect to $GL$ would make us wrongly believe that $P\left(\square \varphi \right)+P\left(\square \neg \varphi \right)\ge 1$. (Everything is provable or refutable or both.)

Of course, the main motivation here is that $GL$ wouldn't get us a naturalistic logical update: we want to be consistent with constraint $\sigma$ by conditioning on the provability of $\sigma$, $\square ┌\sigma ┐$. In $GL$, $\square \psi$ is consistent with $\neg \psi$, so conditioning on new provability facts coming from a theorem prover wouldn't get us much at the object level. We would have to condition on $┌\sigma ┐$ directly, making the role of the theorem prover non-naturalistic. This would (I suspect) be bad news if we then try to apply it to an updateless decision theory.

Updateless Decision Theory

Given that the motivation for naturalistic updates was an updateless one, it wouldn't do to finish the post without at least sketching a UDT based on $P^{\ast }$.

As in UDT 1.5, we have an agent $A\left(\right)$ search for a program with high expected value according to $P^{\ast }\left(\varphi \right)$ and according to a utility function $U\left(\right)$. ($U\left(\right)$ must be encoded in $PA$, so I'll make the assumption that it has natural-numbered values.) Define this as:

$$argma{x}_{p\in programs}{\Sigma }_{x}x\cdot P^{\ast }\left(U\right()=x|A()=p)$$

The set of programs may be finite, for example when operating on a finite machine. In this case, the operation is computable (if infeasible).

Limitations

The above construction is not uniformly coherent. I haven't even shown that it converges to something coherent as we update!

It's not totally clear what happens as we update on constraints provable in $PA$. One concern is that it sounds dangerous to mix $GLS$ with $PA$ -- one might get a system which obeys Lob's theorem but also contains $\square \varphi \to \varphi$. Things should be fine here, because we're effectively just adding arithmetically true statements to $PA$. Although this creates a stronger logic which endorses things like $\neg \square \perp$, the $\square$ still refers to provability in $PA$ rather than provability in the new system.

One thing which I considered in the logical dutch book post which I didn't manage to achieve here is updating on failed proof attempts. Trying to prove something for a long time without success should make us find it less likely. For this purpose, I introduce the notation ${\square }_n\varphi$, which says that there is a proof of $\varphi$ of length at most $n$. We want updating on this to obey conservation of expected evidence:

Conservation of Expected Proof:

• $P\left(\varphi \right)=P\left(\varphi |{\square }_n\psi \right)P\left({\square }_n\psi \right)+P\left(\varphi |\neg {\square }_n\psi \right)P\left(\neg {\square }_n\psi \right)$

Note, however, that this already follows from propositional coherence alone. To make this meaningful, we also want:

Bounded Naturalistic Update

• Where $\sigma$ is a partition of truth, $P(\varphi |{\square }_n┌\sigma ┐)$ is coherent relative to $\sigma$.

This could likely be achieved by enforcing ${\square }_n\varphi \to \square \varphi$ for all $\varphi$, in addition to everything already being enforced in $P^{\ast }\left(\varphi \right)$. Showing that the result is still well-defined and computable requires more than just the decidability of $GLS$, which is why I didn't do this here.

We could then define $P_n\left(\varphi \right)$ by updating sequentially on all our proof attempts, successful or unsuccessful. (Differentiating proof attempts by a length-bound only is very course-grained, but we could make this finer-grained as desired.)

Works Cited:

Paul Christiano. 2014. Non-Omniscience, Probabilistic Inference, and Metamathematics. Technical report 2014–3. MIRI.

Boolos, George. The logic of provability. Cambridge university press, 1995.