I want to echo the other comments thanking you for making this lay-approachable and for the fun format!
I do find myself confused by some of the statements though. It may be that I have a root misunderstanding or that I am misreading some of the more quickly stated sentences.
For example, when you talk about the trees of truth & falsehood and the gap in the middle: am I right in thinking of these trees as provability and non-provability? Rather than perhaps truth & falsehood
Also, in the existence proof for Bs such that P(B|A)>12 and we can prove A→B , you say that if B is a logical truth, A → B must be provable, because anything implies a logical truth. It seems right to me that anything logically implies a logical truth. But surely we can’t prove all logical truths from anything—what if it’s a truth in the grey area such that it can’t be proved at all?
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.
I want to echo the other comments thanking you for making this lay-approachable and for the fun format!
I do find myself confused by some of the statements though. It may be that I have a root misunderstanding or that I am misreading some of the more quickly stated sentences.
For example, when you talk about the trees of truth & falsehood and the gap in the middle: am I right in thinking of these trees as provability and non-provability? Rather than perhaps truth & falsehood
Also, in the existence proof for Bs such that P(B|A)>12 and we can prove A→B , you say that if B is a logical truth, A → B must be provable, because anything implies a logical truth. It seems right to me that anything logically implies a logical truth. But surely we can’t prove all logical truths from anything—what if it’s a truth in the grey area such that it can’t be proved at all?
If someone can put me right, that would be great
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