I’m objecting to an assumption that contradicts a previous assumption which leads to inconsistent PA. If PA is consistent, then we can’t just suppose 1 = 2 because we feel like it. If 1 = 2, then PA is inconsistent and math is broken.
Ah. But in standard math and logic, this is exactly what we do. We can suppose anything because we feel like it.
It sounds like you want something similar to “relevance logic”, in that relevance logic is also a nonstandard logic which doesn’t let you do whatever you want just for the heck of it. I don’t know a whole lot about it, but I think assumptions must be relevant, basically meaning that we actually have to use them. However, afaik, even relevance logic lets us assume things which are contrary to previous assumptions!
Would you also object to the following proof?
Suppose A.
Suppose ¬A.
Contradiction.
So ¬¬A.
So A →¬¬A.
In this proof, I show that A implies its own double negation, but to do so, I have to suppose something contrary to something I’ve already supposed.
Assuming PA is consistent and assuming the agent has crossed, then U for crossing cannot be −10 or the agent would not have crossed. Weird assumptions like “1 = 2” or “the agent proves crossing implies U = −10″ contradict the existing assumption of PA consistency. Any proof that involves inconsistency of PA as a key step is immediately suspect.
Just to emphasize: this is going to have to be a very nonstandard logic, for your notion of which proofs are/aren’t suspect to work.
It is possible that troll bridge could be solved with a very nonstandard logic, of course, but we would also want the logic to do lots of other nice things (ie, support normal reasoning to a very large degree). But it is not clear how you would propose to do that; for example, the proof that a sentence implies its own double negation would appear to be thrown out.
Suppose the agent crosses. Further suppose the agent proves crossing implies 1 = 2. Such a proof means PA is inconsistent, so 1 = 2 is indeed “true” within PA. Thus “agent proves crossing implies 1 = 2″ implies 1 = 2. Therefore by Löb’s theorem, crossing implies 1 = 2.
Putting this in symbols, using box to mean “is provable in PA”:
Suppose □(cross → 1=2).
Suppose the agent crosses.
□1=2
Therefore, cross → □1=2
So □(cross→1=2)→(cross→□(1=2))
See the problem? For Lobs theorem to apply, we need to prove □(a→b)→(a→b). Here, you have an extra box: □(a→b)→(a→□b). So, your proof doesn’t go through.
If the proof leads to “PA is inconsistent”, then every step that follows from that step is unreliable.
Again, I just want to emphasize that this reasoning implies a very nonstandard logic (which probably wouldn’t even support Lob’s theorem to begin with?). Normal logic has no conditions like “you can start ignoring a proof if it starts saying such and such”. Indeed, this would sort of defeat the point of logic: each step is supposed to be individually justified. And in particular, in typical logics (including classical logic, intuitionistic logic, linear logic, and many others), you can assume whatever you want; the point of logic is to study what follows from what, which means we can make any supposition, and see what follows from it. You don’t have to believe it, but you do have to believe that if you assumed it, such-and-such would follow.
Putting restrictions on what we can even assume sounds like putting restrictions on what arguments we’re allowed to listen to, rather than studying the structure of arguments. Logic doesn’t keep people from making bad assumptions; it only tells you what those assumptions imply.
A hypothetical assumption doesn’t harm anybody. If A is totally absurd, that’s fine; we can derive sentences like A→someabsurdthing. The conclusions should be confined to the hypothetical. So, under ordinary circumstances, there is no reason to restrict people from making absurd assumptions. Garbage in, garbage out. No problem.
It’s Lobs theorem that’s letting us take our absurd conclusions and “break them out of the hypothetical” here.
So as I stated before, I think you should be wrestling with Lobs theorem itself here, rather than finding the flaws in other places. I think you’re chasing shadows with your hypothesis about restricting when we can make which assumptions. That’s simply not the culprit here.
I just want to say thanks for taking the time to address my comments. The proof given for the Troll Problem still feels wrong to me but you’re helping me get closer to finding the core of where my intuition is inconsistent with it. I’ll consider what you’ve pointed out and re-examine the problem with a bit more clarity.
Ah. But in standard math and logic, this is exactly what we do. We can suppose anything because we feel like it.
It sounds like you want something similar to “relevance logic”, in that relevance logic is also a nonstandard logic which doesn’t let you do whatever you want just for the heck of it. I don’t know a whole lot about it, but I think assumptions must be relevant, basically meaning that we actually have to use them. However, afaik, even relevance logic lets us assume things which are contrary to previous assumptions!
Would you also object to the following proof?
Suppose A.
Suppose ¬A.
Contradiction.
So ¬¬A.
So A →¬¬A.
In this proof, I show that A implies its own double negation, but to do so, I have to suppose something contrary to something I’ve already supposed.
Just to emphasize: this is going to have to be a very nonstandard logic, for your notion of which proofs are/aren’t suspect to work.
It is possible that troll bridge could be solved with a very nonstandard logic, of course, but we would also want the logic to do lots of other nice things (ie, support normal reasoning to a very large degree). But it is not clear how you would propose to do that; for example, the proof that a sentence implies its own double negation would appear to be thrown out.
Putting this in symbols, using box to mean “is provable in PA”:
Suppose □(cross → 1=2).
Suppose the agent crosses.
□1=2
Therefore, cross → □1=2
So □(cross→1=2)→(cross→□(1=2))
See the problem? For Lobs theorem to apply, we need to prove □(a→b)→(a→b). Here, you have an extra box: □(a→b)→(a→□b). So, your proof doesn’t go through.
Again, I just want to emphasize that this reasoning implies a very nonstandard logic (which probably wouldn’t even support Lob’s theorem to begin with?). Normal logic has no conditions like “you can start ignoring a proof if it starts saying such and such”. Indeed, this would sort of defeat the point of logic: each step is supposed to be individually justified. And in particular, in typical logics (including classical logic, intuitionistic logic, linear logic, and many others), you can assume whatever you want; the point of logic is to study what follows from what, which means we can make any supposition, and see what follows from it. You don’t have to believe it, but you do have to believe that if you assumed it, such-and-such would follow.
Putting restrictions on what we can even assume sounds like putting restrictions on what arguments we’re allowed to listen to, rather than studying the structure of arguments. Logic doesn’t keep people from making bad assumptions; it only tells you what those assumptions imply.
A hypothetical assumption doesn’t harm anybody. If A is totally absurd, that’s fine; we can derive sentences like A→someabsurdthing. The conclusions should be confined to the hypothetical. So, under ordinary circumstances, there is no reason to restrict people from making absurd assumptions. Garbage in, garbage out. No problem.
It’s Lobs theorem that’s letting us take our absurd conclusions and “break them out of the hypothetical” here.
So as I stated before, I think you should be wrestling with Lobs theorem itself here, rather than finding the flaws in other places. I think you’re chasing shadows with your hypothesis about restricting when we can make which assumptions. That’s simply not the culprit here.
I just want to say thanks for taking the time to address my comments. The proof given for the Troll Problem still feels wrong to me but you’re helping me get closer to finding the core of where my intuition is inconsistent with it. I’ll consider what you’ve pointed out and re-examine the problem with a bit more clarity.