I agree with Wei Dai’s solution, though somehow I didn’t see it before. The formula I wrote was incorrect. Do you know why Eliezer is still talking about the problem seven years after Wei Dai provided the solution? Or more specifically, why he wants to have A1 ⊢ ∀P . ◻(A2⊢P) → P instead of A1 ⊢ ∀P . (A2⊢P) → P ?
I’ve rewritten the post, giving credit to Wei Dai, and expanding on my contribution. Does that look okay?
I agree with Wei Dai’s solution, though somehow I didn’t see it before. The formula I wrote was incorrect. Do you know why Eliezer is still talking about the problem seven years after Wei Dai provided the solution? Or more specifically, why he wants to have A1 ⊢ ∀P . ◻(A2⊢P) → P instead of A1 ⊢ ∀P . (A2⊢P) → P ?
I’ve rewritten the post, giving credit to Wei Dai, and expanding on my contribution. Does that look okay?
Your rewrite seems to have the same error as the previous version. A correct formalization of Wei’s solution could look like this:
A1 ⊢ ∀P. (A1 ⊢ P) ↔ (A2 ⊢ P)
If A1=A2, that equation collapses into a tautology, as it should.