Your second case seems really similar to my post about ASP from 2011: http://lesswrong.com/lw/5rq/example_decision_theory_problem_agent_simulates/
You're absolutely right. I know I was in a hurry writing this post, but I don't know how I managed to skip reading the second half of the post that I excerpted.
The other direction follows from the fact that the algorithm is bounded, and PA can simply show the execution trace of in steps.
Unimportant technical point: I think the length of the PA proof grows faster than this. (More precisely, the length in symbols, rather than the length in number of statements; we're almost always interested in the former, since it determines how quickly a proof can be checked or be found by exhaustive search.) The obvious way of showing in PA is to successively show for higher and higher that "after ticks, the Turing machine computing is in the following state, and its tapes have the following content". But even to write out the contents of the tape of a Turing machine that has run for ticks will in general take symbols. So the obvious way of doing the proof takes at least symbols. Moreover, I'm not sure whether we can get from "at time , the configuration is such-and-such" to "at time , the configuration is such-and-such" in a constant number of proof steps. I suspect we don't need more than symbols overall, but I'm not extremely confident. (I'd be quite surprised if the time turned out not to be polynomial, though!)
Note that in both this and the other model of Agent Simulates Predictor, the agent's formal system does not know that the predictor's formal system is consistent. One could argue that in this case it's right to two-box. However, it's still worrisome that the agent's formal system proves $A()=1 \to U()= $0$ and does not prove $A()=1 \to U()= $1000000$, rather than proving both counterfactuals (spuriously) or neither.
There's a certain type of problem where it appears that having more computing power hurts you. That problem is the "agent simulates predictor" Newcomb's Dilemma.
As Gary Drescher put it:
EDITED 5/19/15: There's a formal model of this due to Vladimir Slepnev where the agent and the predictor both have different types of predictive powers, such that in some sense they each know how the other will act in this universe. We'll write this out along with another case where things work out properly.
(One algorithm has more computing power, but the other has stronger axioms: in particular, strong enough to prove that the other formal system is sound, as ZFC proves that PA is sound.)
In one of the following cases, proof-based UDT one-boxes for correct reasons; in the other case, it two-boxes analogously to the reasoning above.
In both cases, we'll use the following lemma:
Lemma: Let A() be an algorithm that returns either 1 or 2, such that ZFC has a proof of length ≈log(N) of "A() returns in ≤N steps". Then ZFC has a proof of length ≈log(N) that "A()=1 if and only if PA proves that A()=1."
Proof: ZFC knows that PA is sound, so ZFC has a short proof that "if PA proves that A()=1, then A()=1". The other direction follows from the fact that the algorithm is bounded, and PA can simply show the execution trace of A in ≤CN steps.
Case 1: Success (Agent Trusts Predictor)
Omega looks through all proofs in PA; when it finds a proof that the agent one-boxes or a proof that the agent two-boxes, it stops looking and fills or empties the box accordingly. (If it fails to prove either, it empties the box.)
The agent looks several times through all proofs in ZFC of length ≤N; it first looks for a proof that one of its actions leads to the payoff $1001000, then $1000000, then $1000, then $0. The first time it finds a proof that an action implies the outcome it's looking for, it immediately takes that action. (If it fails to find any such proof, it two-boxes.)
I claim that for sufficiently large N, the agent one-boxes, and Omega fills the box.
Proof: We use the Lemma. ZFC proves in ≤N steps that A()=1↔□PA[A()=1]. Since we (from outside the problem) assume ZFC is consistent, it will not be able to prove that two-boxing gets it $1001000, nor that one-boxing gets it $1001000, nor that two-boxing gets it $1000000, but it will be able to prove that one-boxing gets it $1000000. Thus it one-boxes. Since it runs in finite time, of course PA proves it one-boxes, and so Omega fills the box.
Case 2: Failure (Agent Simulates Predictor)
We'll swap the deductive processes this time. Omega looks through all proofs in ZFC of length ≤N; when it finds a proof that the agent one-boxes or a proof that the agent two-boxes, it stops looking and fills or empties the box accordingly. (If it fails to prove either, it empties the box.)
The agent looks several times through all proofs in PA; it first looks for a proof that one of its actions leads to the payoff $1001000, then $1000000, then $1000, then $0. The first time it finds a proof that an action implies the outcome it's looking for, it immediately takes that action. (If it fails to find any such proof, it two-boxes.)
I claim that the agent two-boxes, and Omega leaves the box empty.
Proof: Again, by the lemma, ZFC proves that Ω()=1↔□PA[Ω()=1] (where Ω()=1 means "Omega predicts one-boxing and thus fills the box"). Now note that Ω()=1 implies that PA proves $A()=2 \to U=$1001000$ and does not prove that $A()=1 \to U=$1001000$, and thus in this case A()=2; and similarly, Ω()=2 implies that PA proves $A()=2 \to U=$1000$ and does not prove any of the prior counterfactuals, so again A()=2. All of these proofs are quick within ZFC, so Ω does prove that A()=2, and thus Ω()=2.