An Introduction to Löb's Theorem in MIRI Research

I am stuck at part 2.2: "So in particular, if we could prove that mathematics would never prove a contradiction, then in fact mathematics would prove that contradiction"

I've spend 15 minutes on this, but still cannot see relation to löb's theorem. Even though it seems like it should be obvious to attentive reader.

Could anyone please explain or link me to an explanation?

Perhaps this is the wrong venue, but I'm curious how this work generalizes and either applies or doesn't apply to other lines of research.

Schmidhuber's group has several papers on "Goedel machines" and it seems like they involve the use of proofs to find self-rewrites.

We present the first class of mathematically rigorous, general, fully self-referential, self-improving, optimally efficient problem solvers. Inspired by Kurt Gödel's celebrated self-referential formulas (1931), a Gödel machine (or 'Goedel machine' but not 'Godel machine') rewrites any part of its own code as soon as it has found a proof that the rewrite is useful, where the problem-dependent utility function and the hardware and the entire initial code are described by axioms encoded in an initial proof searcher which is also part of the initial code.

Their 2005 paper "Completely Self-Referential Optimal Reinforcement Learners" explained the design and their 2012 paper "Towards an Actual Gödel Machine Implementation" seems to be working towards making something vaguely practical. This is the same group whose PhD students helped founded of DeepMind (like Shane Legg as founder and several others as very early employees). Deepmind was then acquired by Google in 2014.

Since that architecture uses a theorem proving system, and creates new versions of itself, and can even replace its own theorem proving system, it naively seems like the Löbstacle might come up. Are you familiar with Schmidhuber's group's work? Does it seem like their work will run into the Löbstacle and they're just not talking about it? Or does it seem like their architecture makes worries about the Löbstacle irrelevant via some clever architecting?

Basically, my question is "The Löbstacle and Gödel Machines... what's up with them?" :-)

Actually, why is it that when the Lobian obstacle is discussed that it seem to always be in reference to an AI trying to determine if a successor AI is safe, and not an AI trying to determine whether or not it, itself, is safe?

Question: If we do manage to build a strong AI, why not just let it figure this problem out on its own when trying to construct a successor? Almost definitionally, it will do a better job of it than we will.

Similar to V_V's comment. I'm only a layman, but I don't understand one of the first steps.

The paper appears to jump straight into the logic, justifying itself (pardon the pun) by a statement about the intricacies of formal systems proving things about other formal systems.

Can you explain how and why all AI systems correspond to formal systems - what precisely you mean by 'formal system'?

(Btw, I have in fact read GEB, but I am still unable to confidently define a formal system.)

Or a better question might be "Why does this need to be possible within the realms of formal logic to be doable at the level of code/AI? There are many general problems intractable as part of pure maths, yet many numerical methods exist to solve particular instantiations. Why must this be doable at the level of pure logic?"

To motivate the mathematical sections that follow, let’s consider a toy problem. Say that we’ve designed Deep Thought 1.0, an AI that reasons about its possible actions and only takes actions that it can show to have good consequences on balance. One such action is designing a successor, Deep Thought 2.0, which has improved deductive abilities. But if Deep Thought 1.0 (hereafter called DT1) is to actually build Deep Thought 2.0 (DT2), DT1 must first conclude that building DT2 will have good consequences on balance.

Why do we think that agents work deductively? Nothing in the AI or cog-sci literature indicates this, and as an "easy case" for simplified treatment, it seems in fact to expand out to the point of seeming impossibility. Are we attacking deductive-only agents because they appear to be sick with a Hard Problem of Vingeian Reasoning?

I haven't read the paper yet (thanks for posting it, anyway), so maybe the answer to my question is there, but there is something about MIRI interest with Löb's theorem that always bugged me, specifically:

Unfortunately, the straightforward way of setting up such a model fails catastrophically on the innocent-sounding step “DT1 knows that DT2’s deductions are reliable”. If we try and model DT1 and DT2 as proving statements in two formal systems (one stronger than the other), then the only way that DT1 can make such a statement about DT2’s reliability is if DT1 (and thus both) are in fact unreliable! This counterintuitive roadblock is best explained by reference to Löb’s theorem, and so we turn to the background of that theorem.

Sure, DT1 can't prove that DT2 decisions are reliable, and in fact in general it can't even prove that DT1 itself makes reliable decisions, but DT1 may be able to prove "Assuming that DT1 decisions are reliable, then DT2 decisions are reliable".
Isn't that enough for all practical purposes?

Notice that this even makes sense in the limit case where DT2 = DT1, which isn't necessarily just a theoretical pathological case but can happen in practice when even a non-self-modifying DT1 ponders "Why should I not kill myself?"

Am I missing something?
Isn't Löb's theorem just essentially a formal way of showing that you can't prove that you are not insane?