It's nice that more people are starting to think about AI-related logic issues. But I don't understand this part:

When we set them equivalent, we get A1 ⊢ ∀t. ∀P. [[t]]P → P which is okay.

Why is it okay? It seems to me that if the AI can prove ∀t. ∀P. [[t]]P → P, then it can prove that ∀P. (∃t. [[t]]P) → P and blow up by Löb's Theorem again. Like this:

1. Assume that ∃t. [[t]]P

2. Apply your statement and obtain ∃t. P

3. Note that t is unused and obtain P

Also, here's Wei Dai's solution from the original SL4 thread, which seems correct to me:

I think you probably misunderstood the paper. The purpose of searching for new theorem provers is to speed up the theorem proving, not to be able to prove new theorems that were unprovable using the old theorem prover. So the Gödel Machine only needs to prove that the new prover will prove a theorem if and only if the current prover will. I don't think this should be a problem.