The terms "weak induction" and "strong induction" are not commonly used in the study of logic. The terms are commonly used only in books aimed at teaching students how to write proofs. Here are their prototypical symbolic forms: - weak induction: $(\Phi(0) \land (\forall n) [ \Phi(n) \to \Phi(n+1)]) \to (\forall n) \Phi(n)$ - strong induction: $(\Psi(0) \land (\forall n) [ (\forall m \leq n) \Psi(m) \to (\forall m \leq n+1) \Psi(m)]) \to (\forall n) \Psi(n)$ The thing to notice is that "strong" induction is almost exactly weak induction with $\Phi(n)$ taken to be $(\forall m \leq n)\Psi(n)$. In particular, strong induction is not actually stronger, it's just a special case of weak induction modulo some trivialities like replacing $\Psi(0)$ with $(\forall m \leq 0 )\Psi(m)$. Of course you can write variations of the symbolic forms, but the same point applies to all of them: "strong" induction is essentially just weak induction whose induction hypothesis has a bounded universal quantifier. So the question is not why we still have "weak" induction - it's why we still have "strong" induction when this is not actually any stronger. My opinion is that the reason this distinction remains is that it serves a pedagogical purpose. The first proofs by induction that we teach are usually things like $\forall n \left [ \sum_{i=0}^n = n(n+1)/2 \right ]$. The proofs of these naturally suggest "weak" induction, which students learn as a pattern to mimic. Later, we teach more difficult proofs where that pattern no longer works. To give a name to the difference, we call the new pattern "strong induction" so that we can distinguish between the methods when presenting a proof in lecture. Then we can tell a student "try using strong induction", which is more helpful than just "try using induction". In terms of logical strength in formal arithmetic, as you can see above, the two forms are equivalent over some weak base theory as long as you are looking at induction for a class of formulas that is closed under bounded universal number quantification. In particular, all the syntactic classes of the analytical and arithmetical hierarchies have that property, so weak induction for $\Sigma^0_k$ formulas is the same as strong induction for $\Sigma^0_k$ formulas, weak induction for $\Pi^1_k$ formulas is the same as strong induction for $\Pi^1_k$ formulas, and so on. This equivalence will hold under any reasonable formalization of "strong" induction - I chose mine above to make the issue particularly obvious.