When you have a self-referential sentence, it does no good to prove it in the “real world”, because the commonsense logic we use in the “real world” becomes inconsistent when applied to self-referential statements. (“This statement is false.”) You really need a proof of your statement within the formal system. And within the system, the proof you gave doesn’t work: the system cannot prove that falsity improves non-provability, because that would be the system assuming its own consistency all over again. So the long derivation is needed after all.
I agree that the system can’t use this argument, but that doesn’t mean the argument doesn’t work, just like your argument for why your algorithm must defect against a program that always defects.
The difference between my argument and “this statement is false” is that by directly depending on its own truth, “this statement is false” leaves its truth or falsity insufficiently defined. But “this statement is true iff it is provable” depends not directly on its truth but on provability, which is already defined. So I think that my “real world” argument does establish that the statement will be true also within a formal system, even though a formal system cannot establish it with this argument.
Um, “this statement is true iff it is provable” directly depends on both truth and provability. It does refer to its own “platonic” truth value in the “real world”.
When you have a self-referential sentence, it does no good to prove it in the “real world”, because the commonsense logic we use in the “real world” becomes inconsistent when applied to self-referential statements. (“This statement is false.”) You really need a proof of your statement within the formal system. And within the system, the proof you gave doesn’t work: the system cannot prove that falsity improves non-provability, because that would be the system assuming its own consistency all over again. So the long derivation is needed after all.
I agree that the system can’t use this argument, but that doesn’t mean the argument doesn’t work, just like your argument for why your algorithm must defect against a program that always defects.
The difference between my argument and “this statement is false” is that by directly depending on its own truth, “this statement is false” leaves its truth or falsity insufficiently defined. But “this statement is true iff it is provable” depends not directly on its truth but on provability, which is already defined. So I think that my “real world” argument does establish that the statement will be true also within a formal system, even though a formal system cannot establish it with this argument.
Um, “this statement is true iff it is provable” directly depends on both truth and provability. It does refer to its own “platonic” truth value in the “real world”.
It refers to its truth value but not in a paradox generating way.