I am studying analysis 1 by Tao. And here is the definition of strong induction in his book.
Strong induction: Let $m_0$ be a natural number,and let $P(m)$ be a property pertaining to an arbitrary natural number $m$. Suppose that for each $m≥m_0$, we have the following implication: if $P(m')$ is true for all natural numbers $m_0≤m'<m$, then $P(m)$ is also true.(In particular, this means that $P(m_0)$ is true, since in the case the hypothesis is vacuous.) Then we can conclude that $P(m)$ is true for all natural numbers $m≥m_0$.
I saw in few posts on MSE including Strong Induction Requires No Base Case?
I saw that write the strong induction as $$ ∀m ≥m_0[ ∀m'(m_0≤m'<m \implies P(m'))] \implies P(m)$$ But according to me the logical form would look like this $$ ∀m[ ∀m_0≤m'<m, P(m')] \implies P(m)$$
My Question: why people are introducing extra implication? that is $$ ∀m'(m_0≤m'<m \implies P(m')).$$
