PA+100 cannot always predict modal UDT

jessica-liu-taylor

PA+100 cannot always predict modal UDT

post by jessicata (jessica.liu.taylor) · 2015-05-12T20:26:53.000Z · LW · GW · 3 comments

Summary: we might expect $P A + m$ to be able to predict the behavior of an escalating modal UDT agent using $P A + n$ for $n < m$ . However, this is not the case. Furthermore, in environments where $P A + m$ predicts the agent, escalating modal UDT can be outperformed by a constant agent.

For a given logic $X$ , we can define $X + 1 = X + Con (X)$ (i.e. $X + 1$ has all the axioms of $X$ plus the axiom that $X$ is consistent). We can iteratively get $X + 2 = (X + 1) + 1$ and so on.

Now consider $P A + 100$ . In some sense, it is "more powerful" than PA: it contains additional correct axioms. Therefore, we might find it plausible that $P A + 100$ can always correctly predict the behavior of a modal UDT agent using PA.

Ordinary modal UDT can run into issues on some environments due to later stages not be able to use the assumption that logics used in previous stages are consistent. Therefore, define escalating modal UDT to be the same as modal UDT except that the $n$ th proof search uses $P A + n$ instead of $P A$ . Benja might write a post explaining this system better.

Let $m$ be a number higher than the number of proof searches escalating modal UDT makes. Patrick made the conjecture that if $U$ is a simple function of $A ()$ (the agent's output) and $P A + m ⊢ A () = a$ (for each action $a$ , whether the predictor predicts the agent takes action $a$ ), where $A ()$ is escalating modal UDT, then:

The predictor is correct (if $A () = a$ then $P A + m ⊢ A () = a$ )
The agent picks the best action conditioned on the predictor being correct (i.e. the action $a$ that maximizes utility when $A () = a$ and $P A + m ⊢ A () = a$ )

Both parts of the conjecture turn out to be false. First, consider the following environment:

def U():

if $A () = α$

if $P A + 100 ⊢ A () = β$

return 10

else

return 0

else

return 5

First, the agent will determine $P A ⊢ A () = α \to U () = 10$ . For this to be the case $P A$ would have to prove $□_{P A + 100} ┌ A () = β ┐$ . But if $P A$ proves this, then in fact $A () = α$ , so this would require $P A + 100$ to be unsound. Therefore this proof search fails.
Next, the agent will determine $P A + 1 ⊢ A () = β \to U () = 10$ . This obviously fails.
Next, the agent will determine $P A + 2 ⊢ A () = α \to U () = 5$ . This obviously fails.
Next, the agent will determine $P A + 3 ⊢ A () = β \to U () = 5$ . This obviously succeeds, and the agent takes action $β$ .

Now consider whether $P A + 100 ⊢ A () = β$ . Consider a model $M$ of $P A + 100$ in which $M ⊨ P A + 100$ $M ⊨ \neg Con (P A + 100)$

Now: $M ⊨ □_{P A} ┌ \neg Con (P A + 100) ┐$ $M ⊨ □_{P A} ┌ □_{P A + 100} ┌ A () = β ┌ ┐$ $M ⊨ □_{P A} ┌ A () = α \to U () = 10 ┐$ $M ⊨ A () = α$

Since $M ⊨ P A + 100$ , we have $P A + 100 ⊬ A () = β$ . This disproves the first part of the conjecture.

For the second part, consider the following environment:

def U():

if $A () = α$

if $P A + 100 ⊢ A () = β$

 return 0

else

 return 10

else

return 5

First, the agent will determine $P A ⊢ A () = α \to U () = 10$ . This is equivalent to $P A ⊢ \neg □_{P A + 100} ┌ A () = β ┐$ . But $P A$ cannot prove $P A + 100$ consistent, so $P A$ fails to prove this.
Next, the agent will determine $P A + 1 ⊢ A () = β \to U () = 10$ . This obviously fails.
Next, the agent will determine $P A + 2 ⊢ A () = α \to U () = 5$ . This obviously fails.
Next, the agent will determine $P A + 3 ⊢ A () = β \to U () = 5$ . This obviously succeeds, and the agent takes action $β$ .

So, part 2 of the conjecture is false. Escalating modal UDT is outperformed by the agent that always takes action $α$ .

To create predictors that can always predict modal UDT, we may consider having the predictor using $P A + Π_{1}$ (i.e. PA plus all true $Π_{1}$ statements, where $Π_{1}$ is part of the arithmetic hierarchy).

3 comments

Comments sorted by top scores.

comment by orthonormal · 2015-06-20T17:24:46.000Z · LW(p) · GW(p)

The next question I have is whether this non-optimality result holds if the universes are using PA+100 rather than PA. The proof in that post no longer goes through (the expression $□ \neg □ ⊥$ becomes $□_{100} \neg □ ⊥$ , which is of course a tautology). So is there a modal agent which wins at both of those universes?

Replies from: orthonormal

↑ comment by orthonormal · 2015-06-21T20:25:10.000Z · LW(p) · GW(p)

Never mind, that's trivial, you can win at that decision problem via the agent that does one thing if its proof search succeeds and another if its proof search fails.

To generalize, though, if there are N different actions, and for each action there's a decision problem which rewards you iff PA+M proves you take that action, then I think that there exists a decision theory which wins at all of them iff $M \geq N - 1$ . (I think you can inductively prove that the number of possible actions a decision theory can take if PA+m is inconsistent is $\leq m + 1$ .)

comment by orthonormal · 2015-05-26T19:56:30.000Z · LW(p) · GW(p)

I don't think we've defined "escalating modal UDT" on this forum yet; as is clear from context, we mean the agent like the one in this post, except that instead of having a single value of the parameter $ℓ$ , the escalating version increments that parameter every time it fails at finding a proof.

This has the intuitive benefit that the later stages can prove that the earlier stages failed to find a proof (because they know the consistency of all earlier proof systems used).