9 ms·

You're 100% correct. I would be more unequivocal -- saying that the problem is the base case isn't just a little weird, it is incorrect. Your analysis nails it.

dsizzle 5y ago
The “vacuously true” part seems unnecessary (and weirdly subjective). The N=1 base case requires considering N=2 when you apply the inductive step and that fails.
- eperdew 5y ago
  The example I'm about to give is overkill, but I'm trying to make my point very carefully. 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).
  - ashtonbaker 5y ago
    > 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.
  - tsimionescu 5y ago
    But does this do anything meaningful, or is it just pointless drudgery because Coq is a machine and can't 'understand'/assume even simple maths/logic if it isn't explicitly stated? This is not a slight on Coq by any means, just pointing out the difference between human proofs and machine proofs. (Humans can of course be tricked into thinking that subtly false statements are trivially true, which the much more meticulous machine proof would discover) 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?
    - eperdew 5y ago
      I wrote out quite a bit for this, but I think that the main point is that by falling back to the formalism, we see the the LHS of the implication affects our inductive hypothesis. I think this is something that is not clear if you just do "base case starting at n" style proofs." 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.
- Ericson2314 5y ago
  Pre formal methods, sophists spin false proofs like this example. Post formal methods, sophists spin false propositions.
mcphage 5y ago
Their inductive step is perfectly valid. However, requires a group of horses with one removed to still have a horse remaining. Using N=1 is an incorrect base case. Had they proved the N=2 base case, their entire argument would work. Of course, you can’t prove the N=2 base case, so that’s why the argument uses the wrong base case.
- amitkgupta84 5y ago
  The inductive step introduces a premise that “requires a group of horses with one removed to still have a horse remaining.” It is not valid to introduce this premise. The inductive step is not valid.
  - mcphage 5y ago
    The inductive step would work just fine with the correct base case.
    - Jensson 5y ago
      Nah, the inductive step is simply incorrect. For it to be correct it needs to say "for n > 1 the following is true", but it doesn't, the statement isn't true since they forgot to add that part. And if you added "for n > 1" to make the inductive statement correct then it is obvious where the reasoning goes wrong. 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.
      - mcphage 5y ago
        You wouldn't need to add "for n > 2" to the inductive step, any more than you need to include "for n > 1" for arguments where the base step is 1, or "for n > 20" for arguments where the base step is 20.
        5y ago
diffeomorphism 5y ago
Disagree. The induction step works perfectly fine for n>=2. In particular, if you can give me the base case "any two horses have the same color", then this proof works and all horses have the same color. The problem is that the base case is n=2, but the student checked n=0 and n=1.
- wisty 5y ago
  No, the induction step works for n>=3. The induction step fails for n=2. 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.
  - diffeomorphism 5y ago
    tomayto tomahto We are talking about the exact same case. The induction step is n-> n+1 and works perfectly well for n+1=3 horses.
- amitkgupta84 5y ago
  The base case is not n=2, it’s clearly stated as n=1 in the proof. 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.
  - diffeomorphism 5y ago
    We don't even disagree about anything here.... We both say "P(n) => P(n+1)" does not work for n=1, but does work for n>1. 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".

dsizzle 5y ago

The “vacuously true” part seems unnecessary (and weirdly subjective). The N=1 base case requires considering N=2 when you apply the inductive step and that fails.

eperdew 5y ago
The example I'm about to give is overkill, but I'm trying to make my point very carefully. 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).
- ashtonbaker 5y ago
  > 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.
- tsimionescu 5y ago
  But does this do anything meaningful, or is it just pointless drudgery because Coq is a machine and can't 'understand'/assume even simple maths/logic if it isn't explicitly stated? This is not a slight on Coq by any means, just pointing out the difference between human proofs and machine proofs. (Humans can of course be tricked into thinking that subtly false statements are trivially true, which the much more meticulous machine proof would discover) 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?
  - eperdew 5y ago
    I wrote out quite a bit for this, but I think that the main point is that by falling back to the formalism, we see the the LHS of the implication affects our inductive hypothesis. I think this is something that is not clear if you just do "base case starting at n" style proofs." 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.
Ericson2314 5y ago
Pre formal methods, sophists spin false proofs like this example. Post formal methods, sophists spin false propositions.

mcphage 5y ago

Their inductive step is perfectly valid. However, requires a group of horses with one removed to still have a horse remaining. Using N=1 is an incorrect base case. Had they proved the N=2 base case, their entire argument would work. Of course, you can’t prove the N=2 base case, so that’s why the argument uses the wrong base case.

amitkgupta84 5y ago
The inductive step introduces a premise that “requires a group of horses with one removed to still have a horse remaining.” It is not valid to introduce this premise. The inductive step is not valid.
- mcphage 5y ago
  The inductive step would work just fine with the correct base case.
  - Jensson 5y ago
    Nah, the inductive step is simply incorrect. For it to be correct it needs to say "for n > 1 the following is true", but it doesn't, the statement isn't true since they forgot to add that part. And if you added "for n > 1" to make the inductive statement correct then it is obvious where the reasoning goes wrong. 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.
    - mcphage 5y ago
      You wouldn't need to add "for n > 2" to the inductive step, any more than you need to include "for n > 1" for arguments where the base step is 1, or "for n > 20" for arguments where the base step is 20.
      - 5y ago

diffeomorphism 5y ago

Disagree. The induction step works perfectly fine for n>=2. In particular, if you can give me the base case "any two horses have the same color", then this proof works and all horses have the same color. The problem is that the base case is n=2, but the student checked n=0 and n=1.

wisty 5y ago
No, the induction step works for n>=3. The induction step fails for n=2. 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.
- diffeomorphism 5y ago
  tomayto tomahto We are talking about the exact same case. The induction step is n-> n+1 and works perfectly well for n+1=3 horses.
amitkgupta84 5y ago
The base case is not n=2, it’s clearly stated as n=1 in the proof. 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.
- diffeomorphism 5y ago
  We don't even disagree about anything here.... We both say "P(n) => P(n+1)" does not work for n=1, but does work for n>1. 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".