I don’t completely understand how your code corresponds to a proof of Löb’s theorem. Are you assuming that ⊢(☐A→A) holds for all sentences A? In Löb’s theorem it’s assumed to hold only for the sentence P.
I don’t completely understand how your code corresponds to a proof of Löb’s theorem. Are you assuming that ⊢(☐A→A) holds for all sentences A? In Löb’s theorem it’s assumed to hold only for the sentence P.