A simpler technique is to just substitute x = y = 1 in each step and look for the first false equation, i.e., the first step where a false statement is derived from a true statement. Clearly that reasoning step is not valid (does not produce only true conclusions from true premises).
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.
Nice. So here we have two testcases that catch different bugs, and you can never prove the absence of bugs by adding more testcases. But testing still works well enough in practice that people rarely write fully formal proofs for software, or for math theorems for that matter :-)
Our disagreement seems to derive from my use of the words “different flawed step” and your use of “same flaw”. Eliezer suggested substituting 1 for x and y in :
(x+y)(x-y) = y(x-y)
x+y = y
yielding
(1+1)(1-1) = 1(1-1) (true)
1+1 = 1 (false)
Thus, since a true equation was transformed into a false one, the step must have been flawed.
Under my suggestion, we have:
(0+0)(0-0) = 0(0-0) (true)
0+0 = 0 (true)
So, under Eliezer’s suggested criterion (turning true to false) this is not a flawed step, though if you look carefully enough, you can still notice the flaw—a division by zero.
So, under Eliezer’s suggested criterion (turning true to false) this is not a flawed step, though if you look carefully enough, you can still notice the flaw—a division by zero.
Hmm. A failure to identify a flawed step doesn’t mean that the step isn’t flawed.
A true statement turning into a false one does show that you manipulated it badly—but a true statement staying true doesn’t show that you manipulated it well.
For someone that didn’t spend much time in school, you’ve identified one of my chief ways of guessing the teacher’s password. It’s often the case that one can essentially perform this kind of hack to narrow down the options without otherwise understanding the problem as it was intended.
In this case for instance, one can imagine a multiple choice where the answers are the line that was the error. Your solution would rule out lines after a certain point. You might get lucky as a student and have 3 of the 4 answers ruled out this way. Voila! You’ve won and know almost nothing.
Speaking as a mathematican(ok, grad student but close enough for this purpose), this isn’t learning almost nothing. Once one has gone through an example and can see where an attempted proof breaks down one can then look at that part in more detail. Of course one won’t learn much if one only cares about identifying the problematic line, whether in a school setting or another setting; one always needs to generalize and integrate knowledge. Don’t blame the teacher if one isn’t going to take steps to do that.
A simpler technique is to just substitute x = y = 1 in each step and look for the first false equation, i.e., the first step where a false statement is derived from a true statement. Clearly that reasoning step is not valid (does not produce only true conclusions from true premises).
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)
Amusingly, try substituting x=y=0. You find a different flawed step than the one Eliezer found.
Nice. So here we have two testcases that catch different bugs, and you can never prove the absence of bugs by adding more testcases. But testing still works well enough in practice that people rarely write fully formal proofs for software, or for math theorems for that matter :-)
Actually, x=y=0 still catches the same flaw, it just catches another one at the same time.
Our disagreement seems to derive from my use of the words “different flawed step” and your use of “same flaw”. Eliezer suggested substituting 1 for x and y in :
yielding
Thus, since a true equation was transformed into a false one, the step must have been flawed.
Under my suggestion, we have:
So, under Eliezer’s suggested criterion (turning true to false) this is not a flawed step, though if you look carefully enough, you can still notice the flaw—a division by zero.
Hmm. A failure to identify a flawed step doesn’t mean that the step isn’t flawed.
A true statement turning into a false one does show that you manipulated it badly—but a true statement staying true doesn’t show that you manipulated it well.
Hah, this is pretty good :-)
For someone that didn’t spend much time in school, you’ve identified one of my chief ways of guessing the teacher’s password. It’s often the case that one can essentially perform this kind of hack to narrow down the options without otherwise understanding the problem as it was intended.
In this case for instance, one can imagine a multiple choice where the answers are the line that was the error. Your solution would rule out lines after a certain point. You might get lucky as a student and have 3 of the 4 answers ruled out this way. Voila! You’ve won and know almost nothing.
Speaking as a mathematican(ok, grad student but close enough for this purpose), this isn’t learning almost nothing. Once one has gone through an example and can see where an attempted proof breaks down one can then look at that part in more detail. Of course one won’t learn much if one only cares about identifying the problematic line, whether in a school setting or another setting; one always needs to generalize and integrate knowledge. Don’t blame the teacher if one isn’t going to take steps to do that.