As Benja said, I'm imagining that my agents have O(1) calls to a hierarchy of halting agents. But when I write it up, I'll also write up the version with bounded proof limits (where exponentially greater limits correspond to higher oracles), the bounded Löb's Theorem, etc. I'm not too worried, because (as Paul Christiano put it) there are no interesting differences between what you can do in each case; it's simply easier to track things with oracle hierarchies.

I'm not seeing how this goes through. Can you explain how PA+3 can prove that PA through PA+2 won't have found proofs of contrary conclusions?

Hmm. This is a real problem, and I'm thinking about it today.

ETA: Oh, good, Benja's solution works.