Prerequisite: Agents that can predict their Newcomb predictor

(This post is from Benja's backlog of topics that should appear here, which he's deputized me to write up. The original idea was due to Jessica Taylor.)

The phenomena of agent-simulates-predictor or agent-trusts-predictor, where one has stronger axioms and the other has stronger powers of deduction, can be done at various levels of the tradeoff between realistic examples and tractable proofs. In the previous post, I considered the version that uses a bounded proof search on one hand, and a halting oracle on the other. There's a finite version where one process uses a bounded proof search with a much higher bound than the other process. But in this post, I'll discuss the clean infinite version where we pit a halting oracle against an oracle for the next level of the arithmetical hierarchy of Peano Arithmetic.

Here, we'll use two different formal systems built on Peano Arithmetic.

A ${\Pi }_1$ statement of PA is any statement of the form $\forall n\varphi \left(n\right)$, where $\varphi (\cdot )$ uses only bounded quantifiers. (For example, the claim that PA is consistent is a ${\Pi }_1$ sentence, asserting that every natural number is not the Gödel number of a proof of a contradiction.)

$\text{PA}+{\Pi }_1$ is PA plus the (non-decidable in PA) axioms consisting of every ${\Pi }_1$ statement which is true in the standard model of PA. We can think of it as a formal system which can make a call in finite time to a standard halting oracle.

(Note that there's a different meaning of ${\Pi }_1$ for ZFC, involving the analogous definitions for set theory. In order to avoid that ambiguity, we could instead just use the formal system $\text{PA+Sound(PA)}$, which is PA plus the axiom schema $\forall \overrightarrow{n}{\square }_{\text{PA}}\phi \left(\overrightarrow{n}\right)\to \phi \left(\overrightarrow{n}\right)$ for every $\phi$. However, in that case we'd need to go through a proof that $\text{PA+Sound(PA)}$ also knows that $\text{PA}+{\Pi }_1$ is sound.)

We'll have the exact same results as in the last post, so we'll prove the analogous lemma, showing that the stronger axiom system (here, ZFC) can prove that statements of a certain type hold if and only if they are provable by an oracle with weaker axioms but stronger computation (here, $\text{PA}+{\Pi }_1$)

Lemma: Let $\phi$ be a propositional combination of ${\Pi }_1$ statements. Then $\text{ZFC}⊢\phi \leftrightarrow {\square }_{\text{PA}+{\Pi }_1}\phi$.

Proof: First, we note that $\text{ZFC}⊢{\square }_{\text{PA}+{\Pi }_1}\phi \to \phi$ for any $\phi$, because ZFC knows about models of $\text{PA}+{\Pi }_1$, and thus knows it is sound.

Now we show that if $\phi$ is a propositional combination of ${\Pi }_1$ statements, then $\text{ZFC}⊢\phi \to {\square }_{\text{PA}+{\Pi }_1}\phi$. Express $\phi$ in disjunctive normal form; it is thus clear that it suffices to show this for $\phi$ that are conjunctions of ${\Pi }_1$ statements and negations of ${\Pi }_1$ statements. Now if such a $\phi$ holds, then all of its ${\Pi }_1$ substatements must hold, and thus these are axioms of $\text{PA}+{\Pi }_1$; also, all of the negations of ${\Pi }_1$ statements are of the form $\exists n\psi \left(n\right)$ where $\psi$ has only bounded quantifiers, and if this holds, indeed there must be such an $n$ for each substatement, and thus $\text{PA}+{\Pi }_1$ will successfully prove $\phi$. (The inductive argument for this reasoning can be carried out in ZFC.)

Now we can show the same two cases, with the same proofs as before:

Case 1: Agent Trusts Predictor

The agent uses modal UDT and a halting oracle for ZFC; Omega uses the second-level oracle for $\text{PA}+{\Pi }_1$. Note that the statements "$A\left(\right)=1$" and "$A\left(\right)=2$" are each propositional combinations of ${\Pi }_1$ statements about Gödel numbers.

Since we (from outside the problem) believe that ZFC is consistent and we know by the Lemma that Omega will predict correctly, the agent will fail to prove that it can get $1M + $1K by two-boxing or by one-boxing, and will fail to prove that it can get $1M by two-boxing. Then, using the Lemma, it can prove that if it one-boxes, it will get $1M, and so it does.

Case 2: Agent Simulates Predictor

The agent now uses modal UDT as well as a second-level halting oracle for $\text{PA}+{\Pi }_1$; Omega uses a halting oracle for ZFC.

Now, as before, the Lemma implies that Omega can prove that $\Omega \left(\right)=2\to A\left(\right)=2$, and that $\Omega \left(\right)=1\to A\left(\right)=2$, so it proves $A\left(\right)=2$ and does not fill the box; then the agent two-boxes.