That is simpler, because you already optimized it for finding the flaw in that particular incorrect “proof”. I want a technique that generalizes to handle incorrect “proofs” that show 1=3 by setting equal positive and negative square roots, or that all horses are the same color by taking an element from an empty set.
The idea is to replace the reasoning as shown with a simple special case which would have to work if the original was valid.
For instance, in the “horses” example we replace the (more general) inductive step with specific instance where we try to prove that “if all 1 horses are the same colour then all 2 horses are the same colour”.
It’s not guaranteed to work, and even when it does it may not yield all the mistakes (see Perplexed’s comment), but it’s still useful.
The equivalent ‘technique’ in programming, if there is one, is stepping through the code with something like gdb to see where the ‘bug’ happens. The difference is that even when this does catch a bug in progress, it may not be determinate which step should be regarded as the ‘first mistake’. (But adopting conventions, like this usName and sName business, may help.)
does not solve the original problem of making mistakes obvious.
Yes it does.
In all three cases mentioned, it highlights mistakes in the proofs. (Using much less effort than applying massive amounts of paraffin to make each step waterproof.)
I did mean something by this, and not just “making all mistakes obvious”.
The method in the post for handling unsafe strings and a habit of only using reversible operations in some areas of math make the error inherent in not following the convention. The notation takes the same form as the thing being analyzed, moving some thought from a conscious level to an automatic level. This kind of thing can save time overall in many situations because, when a mistake is made, you have already ruled out many places where the mistake cannot be. The paraffin becomes almost invisible, and it eliminates the need to check for leaks.
That is simpler, because you already optimized it for finding the flaw in that particular incorrect “proof”. I want a technique that generalizes to handle incorrect “proofs” that show 1=3 by setting equal positive and negative square roots, or that all horses are the same color by taking an element from an empty set.
Eliezer’s method works in all of those cases.
The idea is to replace the reasoning as shown with a simple special case which would have to work if the original was valid.
For instance, in the “horses” example we replace the (more general) inductive step with specific instance where we try to prove that “if all 1 horses are the same colour then all 2 horses are the same colour”.
It’s not guaranteed to work, and even when it does it may not yield all the mistakes (see Perplexed’s comment), but it’s still useful.
The equivalent ‘technique’ in programming, if there is one, is stepping through the code with something like gdb to see where the ‘bug’ happens. The difference is that even when this does catch a bug in progress, it may not be determinate which step should be regarded as the ‘first mistake’. (But adopting conventions, like this usName and sName business, may help.)
It serves a purpose, but it fails far too often and does not solve the original problem of making mistakes obvious.
Yes it does.
In all three cases mentioned, it highlights mistakes in the proofs. (Using much less effort than applying massive amounts of paraffin to make each step waterproof.)
I did mean something by this, and not just “making all mistakes obvious”.
The method in the post for handling unsafe strings and a habit of only using reversible operations in some areas of math make the error inherent in not following the convention. The notation takes the same form as the thing being analyzed, moving some thought from a conscious level to an automatic level. This kind of thing can save time overall in many situations because, when a mistake is made, you have already ruled out many places where the mistake cannot be. The paraffin becomes almost invisible, and it eliminates the need to check for leaks.
(I did not downvote you, btw)