diff options
| -rw-r--r-- | proof-sketch.txt | 52 |
1 files changed, 51 insertions, 1 deletions
diff --git a/proof-sketch.txt b/proof-sketch.txt index c4cc1e9..3849a3a 100644 --- a/proof-sketch.txt +++ b/proof-sketch.txt @@ -287,7 +287,7 @@ Remarks: A given procedure d3 tries calculate halt3(d, p, i) for only a fixed d, where d represents d3's built-in decider d. -Objection: +Objection 1: I hereby anticipate the following objection to the proof. Surely, if error_decider is found which is similar to should_return_error, @@ -310,6 +310,56 @@ Objection: Furthermore, more than one error_decider exists that can produce the necessary test case. +Objection 2: + + The following objection may be made, which stems from a misunderstanding. + When halting_decider returns error, and that error is erroneous, + it is in fact not erroneous. After all, the halting decider is being + gamed by a trick. The wrapper might print the diagnostic that error + is incorrect, but that doesn't make it incorrect! + + The problem with this objection is that it proceeds from a misunderstanding + about what error means. The three-valued halting decision procedure + contains a boolean procedure for deciding the error case, and it contains + a boolean halting decider. The error return value is a comment upon the + boolean halting decider; it is not a self-referential comment about the + three-valued halting decider. The error value means that the boolean + halting decider is not able to answer true or false (due to trickery). + + In the situation when error is the incorrect value, it can be shown that the + two-valued decider in fact has the correct answer. Only, that answer was + suppressed by the three-valued procedure, due to the should_return_error + subroutine being incorrect. That the correct answer was suppressed by an + incorrect error decision is objectively true, and the program's diagnostic + message is only a remark on that fact. + + How we know that error is an incorrect value is that we can produce + a new version of halting_decider in which we make a correction to the + should_return_error function, but leave the boolean halting decider + exactly the same. When this new halting_decider is plugged into the + wrapper program, with the original error_decider, the new program + will show that the boolean halting decider in fact is correct --- when + the new program is run with the old program's code as its input. + + That is to say, if "program program_code" is reporting that the halting + decider's error return is wrong, we can edit the should_return_error function + inside halting_decider by inverting its boolean value. We then obtain a new + program called "program*". When we run "program* program_code" (new program, + original program's code as argument), this will now confirm that the decider + has returned a correct true or false value. In other words, the underlying + two-valued decider (which does not change between the two programs) correctly + decides whether "program program_code" halts! It is specifically the error + decision in the three-valued decider that was shown wrong by the "program + program_code" test case. + + The goal of this proof is to show that this error decision is not computable, + and that cases exist in which it errs both ways. Since it is not computable, + then a three-valued decider cannot reliably "protect" a two-valued decider + from returning a true or false value. Sometimes the error decision will + incorrectly say "no error", and expose a halting decision which is wrong. + Sometimes it will incorrectly say "error", wrong suppressing a correct + return value from the two-valued decider. + References: [1] _On computable numbers, with an application to the Entscheidungsproblem_, |