Without the very long limit you’ve added, the easy problem becomes formally undecidable as it leads to an infinite regress. In order to return 1, the program has to determine whether it will return 1, and in order to do that it has to determine whether it will return 1, and in order to do that it has to determine whether it will return 1, and..… You’ll use up your 3^^...^^3 iterations and return 0.
Without the limit, the first program would return 1. My proof keeps working almost without modifications. The only change will be that main() will use a while loop instead of an if, which is only used in deriving (2) and doesn’t change its validity. Your argument doesn’t show that the program will never find a proof—it only shows that it can never find the specific proof that you outlined, because it leads to infinite regress or whatever. It will just find another proof instead.
OK. Let’s suppose you successfully write an algorithm a() that can do everything that you said.
Now let’s make some changes. Suppose you were, in the course of your search of proof space, to come across a proof that a() returned 0? You could simply return 0 at that point rather than continuing to search for proofs that a() returned 1. So let’s make that change.
Now comes the fun bit. Change your algorithm a() such that it returns 1 when it hits the iteration limit instead of 0. Not that hard.
Now comes the really fun bit. Invert the output of this algorithm. Let’s call it b(). This function now has the interesting property that it returns 1 when a() returns 0, and vice versa—except in the case where no proofs can be found of a value for a() short of the termination condition, where both now return 0, It’s also interesting that it has exactly the same definition as a() does....
Now let’s make some changes. Suppose you were, in the course of your search of proof space, to come across a proof that a() returned 0? You could simply return 0 at that point rather than continuing to search for proofs that a() returned 1. So let’s make that change.
If you make this change, then step 2 of cousin_it’s proof won’t go through anymore, I think.
What Wei Dai said. The first change you propose breaks A’s ability to obtain step 2 by simple reasoning about itself. Originally I came up with a different problem: systematically search all proofs up to a large length, and if we find a proof that we output some number, then output that number. That problem is way more crazy than mine, I don’t know what the answer is, it might actually depend on the proof checker’s implementation.
Yes, exactly. The proof is a little fussy because it has to keep track of bounded proof lengths everywhere, but it works basically the same.
Does it help you understand the second problem better? It uses the same trick, but with a twist. (You need to get creative when you talk about two proof systems instead of one.)
I still agree with what I said originally about the second problem. You could compare it to these two statements:
A) A is true if and only if A and B are either both provable, or both non-provable.
B) B is true if and only if B and A are either both provable, or both non-provable.
It is much more obvious that both of these statements are necessarily true and provable (by symmetry), than it is that “this is true if and only if it is provable” is true or provable. This is why at first I only accepted the second case.
Actually, after thinking about it more, the statement is obviously provable, without the long derivation.
If “this statement is true iff it is provable” is false, then it naturally cannot be provable. But then it is both false and not provable, which logically implies that it is true iff provable. Therefore it is both true and provable.
So the first program has to output 1 for the same reason.
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”.
Without the very long limit you’ve added, the easy problem becomes formally undecidable as it leads to an infinite regress. In order to return 1, the program has to determine whether it will return 1, and in order to do that it has to determine whether it will return 1, and in order to do that it has to determine whether it will return 1, and..… You’ll use up your 3^^...^^3 iterations and return 0.
It’s a bit like this problem. http://en.wikipedia.org/wiki/Halting_problem
Without the limit, the first program would return 1. My proof keeps working almost without modifications. The only change will be that main() will use a while loop instead of an if, which is only used in deriving (2) and doesn’t change its validity. Your argument doesn’t show that the program will never find a proof—it only shows that it can never find the specific proof that you outlined, because it leads to infinite regress or whatever. It will just find another proof instead.
OK. Let’s suppose you successfully write an algorithm a() that can do everything that you said.
Now let’s make some changes. Suppose you were, in the course of your search of proof space, to come across a proof that a() returned 0? You could simply return 0 at that point rather than continuing to search for proofs that a() returned 1. So let’s make that change.
Now comes the fun bit. Change your algorithm a() such that it returns 1 when it hits the iteration limit instead of 0. Not that hard.
Now comes the really fun bit. Invert the output of this algorithm. Let’s call it b(). This function now has the interesting property that it returns 1 when a() returns 0, and vice versa—except in the case where no proofs can be found of a value for a() short of the termination condition, where both now return 0, It’s also interesting that it has exactly the same definition as a() does....
If you make this change, then step 2 of cousin_it’s proof won’t go through anymore, I think.
What Wei Dai said. The first change you propose breaks A’s ability to obtain step 2 by simple reasoning about itself. Originally I came up with a different problem: systematically search all proofs up to a large length, and if we find a proof that we output some number, then output that number. That problem is way more crazy than mine, I don’t know what the answer is, it might actually depend on the proof checker’s implementation.
So do you also think that this statement is true: “This statement is true if and only if it can be proven to be true”?
See this PDF, paragraph 44.3. It constructs exactly the statement you gave (Henkin’s statement) and proves it’s provable.
Ok, you’ve convinced me. Saying that this statement is true is basically the same as saying program A outputs 1.
Yes, exactly. The proof is a little fussy because it has to keep track of bounded proof lengths everywhere, but it works basically the same.
Does it help you understand the second problem better? It uses the same trick, but with a twist. (You need to get creative when you talk about two proof systems instead of one.)
I still agree with what I said originally about the second problem. You could compare it to these two statements:
A) A is true if and only if A and B are either both provable, or both non-provable. B) B is true if and only if B and A are either both provable, or both non-provable.
It is much more obvious that both of these statements are necessarily true and provable (by symmetry), than it is that “this is true if and only if it is provable” is true or provable. This is why at first I only accepted the second case.
Actually, after thinking about it more, the statement is obviously provable, without the long derivation.
If “this statement is true iff it is provable” is false, then it naturally cannot be provable. But then it is both false and not provable, which logically implies that it is true iff provable. Therefore it is both true and provable.
So the first program has to output 1 for the same reason.
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.