The problem is that the base case is n=2, but the student checked n=0 and n=1.
For n=2, you can't prove h1 is the same colour as h2, because you don't have a h3 to compare it to.
We are talking about the exact same case. The induction step is n-> n+1 and works perfectly well for n+1=3 horses.
The inductive step works fine if you introduce the premise n>=2. It is not valid to introduce that premise. The inductive step is therefore wrong.
The proof in the post is saying the base case is P(1) and the inductive case is that for all n, P(n) => P(n+1)
“P(1)” is true. “For all n, P(n) => P(n+1)” is false. The inductive step is wrong
A completely different proof not present in this post could be:
Base case: P(1) and P(2) Inductive case: for all n > 1, P(n) => P(n+1)
In that completely different proof, the inductive step would be correct and the base case would be wrong. That proof is not in the original post.
I would like to give the student partial credit for the "works for n>1" part and deduct points for the missing n=1 case. The two obvious ways to "fix" that are either giving a proof for "P(1)=>P(2)" (which is currently missing) or establishing P(2) another way and then using induction. Both are fixes of the same thing and not at all "completely different".
If a student was tasked with proving that all horses has the same color given no information about horses then the correct answer is "I can't prove this", the answer given in this article would give 0 points since the student obviously doesn't understand what they are doing. When you check that test, would you mark the base case as the source of the error of the proof, or would you mark the inductive step? The base case is correct, if you marked that part wrong the student would rightfully complain, their logic works there.
You mean to tell me that horses are actually different colors? Really? /s
Anyways, as I said we agree already so no reason to waste further time on this.
Right, the goal here is to find the logical error in an obviously wrong proof, not how to fix this proof as the proof is obviously wrong from the start. You trying to argue how to "fix" it is the one side-tracking the whole thing.
If you say "B wouldn't be wrong if you changed A, so A is wrong!" then that isn't how you find errors. If A is a correct statement and B is an incorrect statement then B is the wrong statement. If you can make B correct by changing A, then B is still an incorrect statement.
If this was a memorization question where you were supposed to find a particular A and B, then you could say that A is wrong even if the statement is correct, since you knew what A and B are supposed to be. But it isn't, we are just here to find the error in the statement to prove that the proof is wrong, we aren't here trying to find a correct version of this statement.
As such, the only data you would need yo prove that all sets of horses are the same color is that all pairs of horses are the same color.
I think zero points would be a very harsh grade given that an understanding of how to do an inductive proof was demonstrated and one minor error was made in an otherwise correct proof.
Who says the question was to demonstrate an inductive proof? Being able to prove that all horses are the same color if all pairs of horses are the same color isn't particularly useful, as typically that would be the definition of all horses having the same color. All that humbug didn't add any extra information to the problem at all, it didn't make things clearer it just made them harder to understand.
Of course, you can’t prove the N=2 base case, so that’s why the argument uses the wrong base case.
In other words, the base case is correct, in all sets of 1 horse all horses has the same color. The inductive step is not correct. Even if you changed the where you put the base case to N=2, the inductive steps reasoning is still wrong as long as it doesn't include the "for n > 1" part.
Note that you can use false intermediate steps like that and still reach a correct conclusion. Then the conclusion is correct but the proof is still wrong since the steps you used were wrong.
This has nothing to do with the idea that it can be common practice to prove claims of the form for all n > N, P(n) by induction when N is a number like 4. Yes there is a perfectly valid way to use proof by induction to do such proofs. Has nothing to do with this blog post.
The blog post glosses over this assumption and thus ends up concluding "p(n) implies p(n+1)" instead of "p(n) implies (n>1 implies p(n+1))”
Suppose you want to prove something for integers >= 2. E.g., suppose you want to prove for all n >= 2, n is positive. The statement you're trying to prove for a given n is actually
P(n) := n >= 2 -> n is positive
Let's prove it by induction.
P(0) is 0 >= 2 -> 0 is positive. P(0) is vacuously true, because 0 < 2.
Suppose P(n). We want to show P(n + 1). Our goal is
n + 1 >= 2 -> n + 1 is positive. Let's break this into the cases n >= 2 and n < 2.
For n >= 2, we assume P(n) and have the LHS of the implies. This gives us n is positive. Say by definition or by a lemma that n positive -> n + 1 is positive, and we handle this branch.
For n < 2, the inductive hypothesis tells us nothing. Assume the LHS of our goal, i.e. n + 1 >= 2. We want to prove n + 1 is positive. Well 2 is positive and therefore n + 1 is positive by transitivity.
This is what I mean by the base case not being special. E.g., in Coq, induction over the natural numbers always starts at 0. When you think about doing induction starting at another number, you're transforming your goal to include something of the form n >= m -> P(n).
The concept of a “minimal base case” really weirded me out but I couldn’t quite put my finger on why. Thanks for the painstaking explanation, this was perspective-broadening.
That is, what is being gained by looking at the vacuously true cases where n<2, when the only interesting base case is the one where the LHS of the implication is true?
As far as drudgery, Coq will solve the trivial cases automatically, so you'd never have to prove the n = 0 case by hand. That said, there's a reason most math is done on paper and not in Coq - there's usually an order of magnitude more detail and drudgery in a formal proof, even with automation.