I feel like this is tightly linked (or could be rephrased as an application of) Gödel’s second incompleteness theorem (a system can’t prove its own consistency). Let me explain:
If we don’t require that Rob is consistent within the hypothetical, he could cross anyway inside of it.
But of course, Rob won’t require Rob to be consistent inside his hypothetical. That is, Rob doesn’t “know” (prove) that Rob is consistent, and so it can’t use this assumption on his proofs (to complete the Löbian reasoning).
Even more concretely in your text:
If so, and if Rob crossed without blowing up, this would result in a contradiction that would prove Rob’s logical system inconsistent. So assuming the consistency of his logical system,[5] by Löb’s Theorem, crossing the bridge would then indeed result in it blowing up. So Rob would conclude that he should not cross.
But Rob can’t assume its own consistency. So Rob wouldn’t be able to conclude this.
In other words, you are already assuming that inside Rob’s system Proof(Blows)→Blows but you need the assumption Con(Rob) to prove this, which isn’t available inside Rob’s system.
We get stuck in a kind of infinite regress. To prove Blows, we need Proof(Blows), and for that Proof(Proof(Blows)) etc. and so the actual conditional proof never takes flight. (Or equivalently, we need Proof(Con(Rob)), and for that Proof(Proof(Con(Rob))), etc.)
This seems to point at embracing hypothetical absurdity as not only a desirable property, but a necessary property of these kinds of systems.
Please do point out anything I might have overlooked. Formalizing the proofs will help clarify the whole issue, so I will look into Adam’s papers when I have more time in case he has gone in that direction.
Thanks, the second bit you quoted, I rewrote. I agree that sketching the proof that way was not good.
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.
This should be more clear and not imply that rob needs to be able to prove his own consistency. I hope that helps.
Okay, now it is clear that you were not presupposing the consistency of the logical system, but its soundness (if Rob proves something, then it is true of the world).
I still get the feeling that embracing hypothetical absurdity is how a logical system of this kind will work by default, but I might be missing something, I will look into Adam’s papers.
I feel like this is tightly linked (or could be rephrased as an application of) Gödel’s second incompleteness theorem (a system can’t prove its own consistency). Let me explain:
But of course, Rob won’t require Rob to be consistent inside his hypothetical. That is, Rob doesn’t “know” (prove) that Rob is consistent, and so it can’t use this assumption on his proofs (to complete the Löbian reasoning).
Even more concretely in your text:
But Rob can’t assume its own consistency. So Rob wouldn’t be able to conclude this.
In other words, you are already assuming that inside Rob’s system Proof(Blows)→Blows but you need the assumption Con(Rob) to prove this, which isn’t available inside Rob’s system.
We get stuck in a kind of infinite regress. To prove Blows, we need Proof(Blows), and for that Proof(Proof(Blows)) etc. and so the actual conditional proof never takes flight. (Or equivalently, we need Proof(Con(Rob)), and for that Proof(Proof(Con(Rob))), etc.)
This seems to point at embracing hypothetical absurdity as not only a desirable property, but a necessary property of these kinds of systems.
Please do point out anything I might have overlooked. Formalizing the proofs will help clarify the whole issue, so I will look into Adam’s papers when I have more time in case he has gone in that direction.
Thanks, the second bit you quoted, I rewrote. I agree that sketching the proof that way was not good.
This should be more clear and not imply that rob needs to be able to prove his own consistency. I hope that helps.
Okay, now it is clear that you were not presupposing the consistency of the logical system, but its soundness (if Rob proves something, then it is true of the world).
I still get the feeling that embracing hypothetical absurdity is how a logical system of this kind will work by default, but I might be missing something, I will look into Adam’s papers.