能否不借助`forall n m, n + S m = S (n + m)`证明`forall n, n + S n = S (n + n)`？

• 结论：可以证明，但直接对n归纳会因归纳假设过弱卡壳，需要加强归纳假设，或者在证明过程中推导所需的特例性质。
• 直接归纳n时的困境：
  当尝试对n进行归纳，得到的归纳假设是IHn: n + S n = S (n + n)，但需要证明的目标是：

  n + S (S n) = S (n + S n)
  

  此时归纳假设无法直接应用，因为假设仅覆盖了n与S n的加法关系，而目标涉及n与S (S n)的关系。

可行的证明思路：加强归纳假设 #

我们可以将命题推广为更一般的形式，并非直接调用被禁止的引理，而是将其证明过程嵌入到目标命题的证明中：

1. 基础情况（n=0）：
   左边：0 + S m = S m（根据加法定义，0加任意数等于该数）
   右边：S (0 + m) = S m（由加法定义，0+m=m，取后继得结果）
   两边相等，基础情况成立。
2. 归纳步骤：假设对n有n + S m = S (n + m)，证S n + S m = S (S n + m)：
   左边：S n + S m = S (n + S m)（加法定义：S p + q = S (p + q)）
   代入归纳假设得：S (S (n + m))
   右边：S (S n + m) = S (S (n + m))（加法定义：S p + q = S (p + q)）
   两边相等，归纳步骤成立。

通过证明这个一般形式，我们自然可以得到当m=n时的特例，也就是目标命题forall n, n + S n = S (n + n)。

另一种思路：直接在目标证明中推导中间步骤 #

如果不愿推广到一般形式，也可以在归纳目标命题的过程中，针对中间出现的n + S (S n) = S (n + S n)单独推导：

• 对这个式子再做一次归纳（比如对n）：
  • 基础情况n=0：0 + S(S0) = S(S0)，S(0 + S0) = S(S0)，两边相等。
  • 归纳步骤：假设p + S(S p) = S(p + S p)，证S p + S(S(S p)) = S(S p + S(S p))，利用加法定义展开两边即可得证。

内容的提问来源于stack exchange，提问作者Yousef Alhessi