关于皮亚诺系统中不存在循环的自证正确性验证问询

嘿，我把皮亚诺系统中「不存在循环」这个结论的完整自证过程整理好了，从基础定义到核心定理的推导逻辑连贯，咱们一步步拆解来看：

皮亚诺系统的定义 #

Definition (Peano systems). Suppose $P$ is a set, $1 \in P$, and $S: P \to P$ is a function. The triple $(P, S, 1)$ is a Peano system if the following conditions hold:

• (P1) $\forall x (1 \neq S(x))$，也就是1不是任何元素的后继；
• (P2) $\forall x \forall y (x \neq y \implies S(x) \neq S(y))$，后继函数是单射；
• (P3) $\forall A ([A \subseteq P \land 1 \in A \land \forall x (x \in A \implies S(x) \in A)] \implies P = A)$，这就是数学归纳法的基础：满足归纳条件的子集必然是全集本身。

迭代定理（核心工具） #

Theorem 1 (Iteration Theorem). Let $(P, S, 1)$ be a Peano system. Suppose $W$ is an arbitrary set, $c \in W$, and $g: P \to W$ is a function. Then, there exists a unique function $f: P \to W$ such that:

• (i) $f(1) = c$，函数在1处的取值为$c$；
• (ii) $\forall x (f(S(x)) = g(f(x)))$，函数满足递归关系。

辅助引理推导 #

引理1：存在唯一的递归函数$f_x$ #

Lemma 1. There exists a unique function $f_x : P \to P$, determined by $x \in P$, such that:

• (i) $f_x(1) = S(x)$；
• (ii) $\forall u (f_x(S(u)) = S(f_x(u)))$.

Proof. Take an arbitrary $x \in P$. Take $W = P$, $c = S(x)$ and $g = S$ in Theorem $1$. 直接套用迭代定理，就能得到这个唯一存在的函数。$\square$

引理2：后继元素对应的函数满足递推关系 #

Lemma 2. Let $x \in P$. $\forall u (f_{S(x)}(u) = S(f_x(u)))$.

Proof. Let $A = {u: u \in P \land f_{S(x)}(u) = S(f_x(u))}$. Clearly, $A \subseteq P$.

1. 首先验证$1 \in A$：$f_{S(x)}(1) = S(S(x)) = S(f_x(1))$，符合条件；
2. 归纳假设：若$u \in A$，则$f_{S(x)}(u) = S(f_x(u))$；
3. 推导后继情况：$f_{S(x)}(S(u)) = S(f_{S(x)}(u)) = S(S(f_x(u))) = S(f_x(S(u)))$，所以$S(u) \in A$；
   由皮亚诺公理(P3)，$P = A$，即对所有$u \in P$结论成立。$\square$

引理3：1不会出现在$f_1$的取值中 #

Lemma 3. $\forall u (1 \neq f_1(u))$.

Proof. Let $A = {u: u \in P \land 1 \neq f_1(u)}$. Clearly, $A \subseteq P$.

1. $1 \in A$：由(P1)，$1 \neq S(1) = f_1(1)$；
2. 归纳假设：若$u \in A$，则$1 \neq f_1(u)$；
3. 推导后继情况：$f_1(S(u)) = S(f_1(u))$，再由(P1)，1不是任何元素的后继，所以$1 \neq S(f_1(u)) = f_1(S(u))$，即$S(u) \in A$；
   由(P3)，$P = A$，结论对所有$u \in P$成立。$\square$

核心结论：皮亚诺系统中无循环 #

Theorem 2. There are no loops in a Peano system. That is, $\forall x \forall u (x \neq f_x(u))$.

Proof. Let $A = {x: x \in P \land \forall u (x \neq f_x(u))}$. Clearly, $A \subseteq P$.

1. $1 \in A$：直接由引理3可得；
2. 归纳假设：若$x \in A$，则对所有$u$，$x \neq f_x(u)$；
3. 推导后继情况：对任意$u$，由(P2)（后继函数是单射）和引理2，$S(x) \neq S(f_x(u)) = f_{S(x)}(u)$，所以$S(x) \in A$；
   由(P3)，$P = A$，即对所有$x,u \in P$，$x \neq f_x(u)$，也就是皮亚诺系统中不存在循环。$\square$

备注：内容来源于stack exchange，提问作者Mostafizur Rahman