feels to me like the problems with Lob’s theorem come from treating worldly cause and effect as logical implication above the proof system, which is just silly. (i’m no expert
That certainly is one of the problems. Even if the world actually is a formal system in some sense, how can an agent prove that it is?
This is beside this whole class of agents just being inconsistent: formal systems that can generally prove Prov(P) → P (as is assumed here for the use of Löb’s theorem) are known by Gödel’s 2nd incompleteness theorem to be inconsistent.
feels to me like the problems with Lob’s theorem come from treating worldly cause and effect as logical implication above the proof system, which is just silly. (i’m no expert
That certainly is one of the problems. Even if the world actually is a formal system in some sense, how can an agent prove that it is?
This is beside this whole class of agents just being inconsistent: formal systems that can generally prove Prov(P) → P (as is assumed here for the use of Löb’s theorem) are known by Gödel’s 2nd incompleteness theorem to be inconsistent.
Don’t know what part of the post you’re referring to.