Yes you are right that the first tree is provability, but I think the second tree is meant to be disprovability rather than non-provability. Similarly, when the OP later talks about “logical truths” and “logical falsehoods” it seems he really means “provable statements” and “disprovable statements”—this should resolve the issue in your last paragraph, since if B is provable then so is A->B.
Similarly, when the OP later talks about “logical truths” and “logical falsehoods” it seems he really means “provable statements” and “disprovable statements”—this should resolve the issue in your last paragraph, since if B is provable then so is A->B
If that’s the case, then how does Goedel kick in? He then says, nothing can separate logical truth from logical falsehood. But if he means provability and disprovability, then trivially they can be separated
Here “separation” would mean that there is an algorithm which inputs any statement and outputs either “yes” or “no”, such that the algorithm returns “yes” on all inputs that are provable statements and “no” on all inputs that are disprovable statements. But the algorithm also has to halt on all possible inputs, not just the ones that are provable or disprovable. Such a separation algorithm cannot exist (I am not sure if this follows from Gödel’s theorem or requires a separate diagonalization argument). This is the result needed in that step of the argument.
Yes you are right that the first tree is provability, but I think the second tree is meant to be disprovability rather than non-provability. Similarly, when the OP later talks about “logical truths” and “logical falsehoods” it seems he really means “provable statements” and “disprovable statements”—this should resolve the issue in your last paragraph, since if B is provable then so is A->B.
Yeah, you’re definitely right there. Oops, me.
If that’s the case, then how does Goedel kick in? He then says, nothing can separate logical truth from logical falsehood. But if he means provability and disprovability, then trivially they can be separated
Here “separation” would mean that there is an algorithm which inputs any statement and outputs either “yes” or “no”, such that the algorithm returns “yes” on all inputs that are provable statements and “no” on all inputs that are disprovable statements. But the algorithm also has to halt on all possible inputs, not just the ones that are provable or disprovable. Such a separation algorithm cannot exist (I am not sure if this follows from Gödel’s theorem or requires a separate diagonalization argument). This is the result needed in that step of the argument.
Ah, so I was quite wrong when I said “trivially they can be separated”. Cos we only have semi-decision procedures for provability and disprovability!
Thanks for helping me with this