Thanks for the comment. tl;dr, I think you mixed up some things I said, and interpreted others in a different way than I intended. But either way, I don’t think there are “enormous problems”.
So the statement to be proven (which I shall call P) is not just “agent takes action X”, but “when presented with this specific proof of P, the agent takes action X”.
Remember that I intentionally give a simplified sketch of the proof instead of providing it. If I did, I would specify the provability predicate. I think you’re conflating what I say about the proof and what I say about the agent. Here, I say that our model agent who is vulnerable to spurious proofs would obey a proof that it would take X if presented. Demski explains things the same way. I don’t say that’s the definition of the provability predicate here. In this case, an agent being willing to accede proofs in general that it will take X is indeed sufficient for being vulnerable to spurious proofs.
Second is that in order for Löb’s theorem to have any useful meaning in this context, the agent must be consistent and able to prove its own consistency, which it cannot do by Gödel’s second incompleteness theorem.
I don’t know where you’re getting this from. It would be helpful if you mentioned where. I definitely don’t say anywhere that Rob must prove his own consistency, and neither of the two types of proofs I sketch out assume this either. you might be focusing on a bit that I wrote: “So assuming the consistency of his logical system...” I’ll edit this explanation for clarity. I don’t intend that Rob be able to prove the consistency, but that if he proved crossing would make it blow up, that would imply crossing would make it blow up.
As presented, it is given a statement P (which could be anything), and asked to verify that “Prov(P) → P” for use in Löb’s theorem.While the post claims that this is obvious, it is absolutely not.
I don’t know where you’re getting this from either. In the “This is not trivial...” paragraph I explicitly talk about the difference between statements, proofs, and provability predicates. I think you have some confusion about what I’m saying either due to skimming or to how I have the word “hypothetically” do a lot of work in my explanation of this (arguably too much). But I definitely do not claim that “Prov(P) → P”.
Here’s the new version of the paragraph with my mistaken explanation fixed.
“Suppose that hypothetically, Rob proves that crossing the bridge would lead to it blowing up. Then if he crossed, he would be inconsistent. And if so, the troll would blow up the bridge. So Rob can prove that a proof that crossing would result in the bridge blowing up would mean that crossing would result in the bridge blowing up. So Rob would conclude that he should not cross. ”
Thanks for the comment. tl;dr, I think you mixed up some things I said, and interpreted others in a different way than I intended. But either way, I don’t think there are “enormous problems”.
Remember that I intentionally give a simplified sketch of the proof instead of providing it. If I did, I would specify the provability predicate. I think you’re conflating what I say about the proof and what I say about the agent. Here, I say that our model agent who is vulnerable to spurious proofs would obey a proof that it would take X if presented. Demski explains things the same way. I don’t say that’s the definition of the provability predicate here. In this case, an agent being willing to accede proofs in general that it will take X is indeed sufficient for being vulnerable to spurious proofs.
I don’t know where you’re getting this from. It would be helpful if you mentioned where. I definitely don’t say anywhere that Rob must prove his own consistency, and neither of the two types of proofs I sketch out assume this either. you might be focusing on a bit that I wrote: “So assuming the consistency of his logical system...” I’ll edit this explanation for clarity. I don’t intend that Rob be able to prove the consistency, but that if he proved crossing would make it blow up, that would imply crossing would make it blow up.
I don’t know where you’re getting this from either. In the “This is not trivial...” paragraph I explicitly talk about the difference between statements, proofs, and provability predicates. I think you have some confusion about what I’m saying either due to skimming or to how I have the word “hypothetically” do a lot of work in my explanation of this (arguably too much). But I definitely do not claim that “Prov(P) → P”.
Here’s the new version of the paragraph with my mistaken explanation fixed.
“Suppose that hypothetically, Rob proves that crossing the bridge would lead to it blowing up. Then if he crossed, he would be inconsistent. And if so, the troll would blow up the bridge. So Rob can prove that a proof that crossing would result in the bridge blowing up would mean that crossing would result in the bridge blowing up. So Rob would conclude that he should not cross. ”