关于二阶量化中实质条件句被视为逻辑蕴含的原因及皮亚诺二阶归纳公理的相关技术疑问

根据维基百科对数学归纳法形式化的内容，二阶归纳公理的表述如下：
$$\forall P(P(0)\land \forall k(P(k) \to P(k+1)) \to \forall x(N(x) \to P(x))$$
这里的$N(x)$表示“$x$是自然数”。原文章里默认了变量$x$的自然数属性，我特意把这个条件补充进公理中，让整个表述更清晰明确。这条公理也和其他皮亚诺公理一起，在皮亚诺算术的相关介绍里有非正式的说明。

维基百科的皮亚诺算术词条里有这么个说法：“每个自然数都可以通过对0多次应用后继运算得到”这个直观概念，需要一条额外的公理来支撑——也就是有时被称为归纳公理的那条。不过最开始我看到这个说法时，觉得它好像是错的。我的推理过程大概是这样的……

备注：内容来源于stack exchange，提问作者Electro-blob