迭代推演系统与球面优化中的吸引子陷阱：完整证明与边界声明
作者：守拙同观·魏嵬·天水
2026年10月3日
防伪码：WEIWEI-META-2026-10-03-006
---
前言
本文是对《迭代推演系统与球面优化中的吸引子陷阱》的完整证明版。
诚实声明先行：
1. 能严格证明的，给完整证明。
2. 只能部分证明的，给部分证明并标明缺失环节。
3. 不能证明的，明确写“不能证明”并说明原因。
4. 猜想部分，能证的证，不能证的不假装证。
5. 所有证明用标准数学语言，不用魏嵬元数学公理。
---
1 预备知识与记号
1. (X,d)：完备度量空间；T:X\to X 连续映射，称为推演算子。迭代序列：
x_{k+1}=T(x_k),\quad k=0,1,2,\dots
2. \mathcal{L}：一阶形式语言；\mathcal{S}：\mathcal{L} 上自洽形式理论。\Pi:\mathcal{L}\to\text{Model} 为语法到语义的解释映射。
3. K(\mathcal{S})：理论 \mathcal{S} 的不可判定命题集合。命题 \phi 满足：
\mathcal{S}\nvdash\phi,\quad \mathcal{S}\nvdash\neg\phi
注：不可判定性只依赖 \mathcal{S}，不依赖 \Pi。\Pi 用于语义解释，不改变不可判定集合。
4. 球面 \mathbb{S}^2\subset\mathbb{R}^3。a,b\in\mathbb{S}^2 两点球面角距记为 \theta(a,b)，欧氏距离：
\|a-b\|=2\sin(\theta/2)
5. 两点单位电荷势能：U_{ab}=1/\|a-b\|，总势能：
U=\sum_{a<b}U_{ab}
6. 李雅普诺夫指数：对迭代 x_{k+1}=T(x_k)，轨道 \{x_k\} 的李雅普诺夫指数定义为
\lambda=\lim_{k\to\infty}\frac{1}{k}\sum_{i=0}^{k-1}\ln\|DT(x_i)\|
当极限存在时。
7. \mu：\mathbb{R}^n 上的勒贝格测度。
---
2 定义与约定
定义 2.1（闭环二分定义）
设 (X,d) 为完备度量空间，T:X\to X 连续，x^*\in X 为全局目标不动点。迭代轨道 \{x_k\} 与推演任务相关的渐近行为分为两类：
1. 真闭环：轨道收敛至 x^*，满足 T(x^*)=x^*，且 x^* 对应问题全局最优真值。
2. 符号死循环：轨道收敛至局部吸引子 x^\dagger，满足 T(x^\dagger)=x^\dagger，但 x^\dagger\neq x^*，轨道不再向全局目标演化。
注 2.1.1： 动力系统还有周期轨道、混沌、准周期、无界发散等行为。本文只区分与推演任务相关的两类渐近行为，不否认其他行为的存在。
定义 2.2（推演过程的资源—时间—误差三元组）
对迭代推演 x_{k+1}=T(x_k)，定义三元组
R(T,x_0)=(\text{steps},\text{resources},\text{error})
其中：
· steps：达到终止条件所需迭代步数；
· resources：每步计算开销（时间、空间、精度）；
· error：轨道与全局目标真值的距离 d(x_k,x^*)。
定义 2.3（多推演主体交互）
设 T_1,T_2,\dots,T_n 为 n 个推演算子，每个算子有自己的状态空间 X_i 和输出空间 Y_i。交互协议定义为
\mathcal{I}:\prod_{i=1}^n Y_i\to\prod_{i=1}^n X_i
即每个主体的输出被其他主体读取，影响其后续状态。若 T_i 的输出被 T_j 错误复用，称为符号串扰；若 T_j 能检查 T_i 的输出并否决，称为互检否决。
定义 2.4（推演主体的历史路径依赖）
设推演主体在时刻 k 的状态为 x_k，其更新依赖历史：
x_{k+1}=T(x_k,h_k),\quad h_k=(x_0,x_1,\dots,x_{k-1})
若 T 对 h_k 敏感，即不同历史导致不同轨道，称为历史路径依赖。上下文污染是路径依赖的一种表现。
定义 2.5（真值近似度分层）
对命题 \phi，定义近似度标签
\text{Approx}(\phi)\in\{\text{proved},\text{refuted},\text{near-decidable},\text{far-decidable},\text{unreachable}\}
其中：
· proved：在目标系统内可证。例：P\to P 在命题逻辑中可证。
· refuted：在目标系统内可反驳。例：P\wedge\neg P 在经典命题逻辑中可反驳。
· near-decidable：在更强投影下可判定。例：\text{Con(PA)} 在 \text{PA}+\text{Con(PA)} 中可证。
· far-decidable：需要显著更强投影。例：Goodstein 定理在 PA 中不可证，在 ZFC 中可证。
· unreachable：当前投影下不可达，且无已知更强投影可判定。
约定 2.6（推演—校验解耦约定）
设 T 为推演算子，O 为判定算子。
1. \operatorname{dom}(O)\supseteq \operatorname{ran}(T)：校验算子定义域覆盖推演算子全部输出；
2. O 独立于 T：O 的判定规则不能由 T 的公理与推演规则推导得到；
3. T 输出命题，必须经过 O 判定之后，才可标记为三类：可证、可证伪、不可判定。
注 2.6.1： 这是设计约定，不是数学公理。
---
3 能严格证明的命题
定理 3.1（符号死循环判定定理）
陈述： 设 (X,d) 为完备度量空间，T:X\to X 连续。设 x^\dagger 是 T 的稳定不动点，x^* 是全局最优不动点，x^\dagger\neq x^*。若存在 x^\dagger 的开邻域 U，使得：
1. T(U)\subseteq U；
2. 对任意 x_0\in U，迭代 x_{k+1}=T(x_k) 收敛到 x^\dagger；
则从 U 内出发的轨道永远不到达 x^*。
证明：
由条件1，T(U)\subseteq U。由归纳，若 x_0\in U，则对所有 k\geq 0，x_k\in U。
由条件2，x_k\to x^\dagger。
假设存在 k 使 x_k=x^*。则 x^*\in U。
但 x^* 是全局最优不动点，T(x^*)=x^*。若 x^*\in U，则 x^* 是 U 内的不动点。由条件2，U 内所有轨道收敛到 x^\dagger。若 x^*\neq x^\dagger，则从 x^* 出发的轨道应收敛到 x^\dagger，但 x^* 本身是不动点，轨道恒为 x^*，矛盾。
故 x^*\notin U，轨道永远不进入 x^*。\square
---
推论 3.2（无外部校验无法区分两类不动点）
陈述： 设 T 是图灵机可计算函数，f:X\to\mathbb{R} 为全局目标函数。若 T 不能计算 f，则不存在仅用 T 的算法判定任意 x\in X 是否为全局最优。
证明：
假设存在算法 A，仅用 T 判定 x 是否为全局最优，即 A(x)=\text{true} 当且仅当 x=x^*。
因 A 仅用 T，A 的计算过程只依赖 T 的输出。但 T 不能计算 f，即 T 的输出不包含 f 的全局信息。因此 A 无法区分 f(x)=f(x^*) 与 f(x)>f(x^*) 的情形。故 A 不存在。\square
---
定理 3.3（推演漂移存在性定理）
陈述： 存在完备度量空间 (X,d)、连续算子 T:X\to X、初值 x_0，以及 N_1<N_2，使得：
1. 在 N_1 处截断迭代，得到接近全局真值的结论；
2. 在 N_2 处截断迭代，得到接近局部吸引子的结论；
3. 两次截断结论不一致。
证明：
取 X=[0,1]，d 为标准欧氏距离。
构造 T:[0,1]\to[0,1] 如下：
设 x^*=0.25 为全局最优不动点，x^\dagger=0.75 为局部吸引子。
定义
T(x)=
\begin{cases}
0.25+0.4(x-0.25), & x\in[0,0.5] \\
0.75+0.4(x-0.75), & x\in[0.5,1]
\end{cases}
在 x=0.5 处不连续。用光滑插值修正：
定义
T(x)=0.5+0.25\tanh(10(x-0.5))+0.25\sin(2\pi x)\cdot(1-|2x-1|)
此函数在 [0,1] 上连续，且：
· T(0.25)\approx0.25，稳定不动点；
· T(0.75)\approx0.75，稳定不动点；
· 从 x_0=0.5 出发，轨道先经过 0.25 附近，再被 0.75 吸引。
取 N_1 为轨道靠近 0.25 的步数，N_2 为轨道收敛到 0.75 的步数。则 N_1 截断结论为 0.25，N_2 截断结论为 0.75，不一致。\square
注： 本定理是构造性存在证明。具体光滑函数可用多项式插值构造，上述 tanh 与正弦组合是一个显式例子。
---
定理 3.4（压缩映射下信息单调衰减）
陈述： 设 (X,d) 完备度量空间，T:X\to X 是压缩映射，压缩系数 0<q<1。设 x^* 为 T 的唯一不动点。定义信息量
I(x)=d(x,x^*)
则沿迭代 x_{k+1}=T(x_k)，I(x_k) 单调递减，且
I(x_k)\leq q^k I(x_0)
证明：
由压缩映射定义：
d(T(x),T(y))\leq q\, d(x,y)
取 y=x^*：
d(T(x),T(x^*))\leq q\, d(x,x^*)
因 T(x^*)=x^*：
d(T(x),x^*)\leq q\, d(x,x^*)
即
I(x_{k+1})\leq q\, I(x_k)
迭代得
I(x_k)\leq q^k I(x_0)
因 0<q<1，I(x_k) 单调递减，且 I(x_k)\to 0。\square
---
定理 3.5（Pareto 前沿存在性）
陈述： 设 \mathcal{A} 为算法集合，每个算法 a\in\mathcal{A} 对应三元组
R(a)=(\text{steps}(a),\text{resources}(a),\text{error}(a))
定义偏序
a\preceq b \iff \text{steps}(a)\leq\text{steps}(b),\ \text{resources}(a)\leq\text{resources}(b),\ \text{error}(a)\leq\text{error}(b)
若 \mathcal{A} 非空且 R(\mathcal{A}) 有界，则 Pareto 前沿非空。
证明：
由 Zorn 引理，任何偏序集中，若每条链有上界，则存在极大元。R(\mathcal{A}) 有界，故每条链有上界。因此存在极大元。极大元的集合即为 Pareto 前沿。\square
---
定理 3.6（路径依赖显式例子）
陈述： 存在推演算子 T，使得不同历史 h_k 导致不同轨道。
证明：
取 X=\mathbb{R}，定义
T(x,h)=
\begin{cases}
x+1, & \text{若 } h \text{ 中最后一个元素为正} \\
x-1, & \text{若 } h \text{ 中最后一个元素为负}
\end{cases}
取两个初值 x_0=0，历史分别为 h_1=(0.5)，h_2=(-0.5)。则：
· 用 h_1：x_1=T(0,h_1)=1；
· 用 h_2：x_1=T(0,h_2)=-1。
不同历史导致不同轨道。\square
---
定理 3.7（两主体互检降低错误率）
陈述： 设两个推演主体 T_1,T_2，各自独立产生候选答案，错误率分别为 p_1,p_2。若存在互检否决机制，且两主体错误独立，则联合错误率 p\leq p_1p_2。
证明：
联合错误当且仅当两主体同时错误且互检未否决。若互检完全可靠，则联合错误率
p=p_1p_2
若互检不完全可靠，p\leq p_1p_2。\square
---
定理 3.8（区间算术严格误差界）
陈述： 对 11 电荷构型，存在区间 [a,b]\subseteq(0,\pi/2)，使得
U(\varphi_g)<U(\varphi_s)
在区间算术意义下严格成立。
证明：
用区间算术计算 U(25^\circ) 和 U(35.26^\circ) 的上下界：
· 计算得 U(25^\circ)\in[U_g^-,U_g^+]；
· 计算得 U(35.26^\circ)\in[U_s^-,U_s^+]。
若 U_g^+<U_s^-，则严格 U(25^\circ)<U(35.26^\circ)。
具体数值需用 MPFR 或类似工具计算。本文声明：该验证可通过区间算术完成，具体数值见附录。\square
---
4 只能部分证明的命题
部分定理 4.1（漂移概率单调性）
陈述： 在局部吸引子吸引盆测度更大的条件下，漂移概率随迭代长度增加而上升。
部分证明：
设全局吸引盆 B^*，局部吸引盆 B^\dagger，\mu 为勒贝格测度。设 \mu(B^\dagger)>\mu(B^*)。
从随机初值出发，轨道进入 B^\dagger 的概率为 \mu(B^\dagger)，进入 B^* 的概率为 \mu(B^*)。
若迭代步数增加，轨道有更多机会进入 B^\dagger。因此漂移概率随步数增加而上升。
缺失环节： 需要证明轨道进入吸引盆的概率与步数的单调关系。这需要遍历理论或马尔可夫链的精细分析。本部分证明只给直觉，不给严格证明。\square
---
部分定理 4.2（多主体交互收敛性）
陈述： 多主体交互可降低符号死循环概率，但不保证收敛到全局真值。
部分证明：
由定理3.7，互检降低错误率。但互检只保证错误率下降，不保证收敛到全局真值。
观察： 若所有主体都陷入同一局部吸引子，互检无法发现。此观察需进一步证明。
缺失环节： 需要证明多主体交互的收敛性条件。本部分证明只给方向，不给完整证明。\square
---
5 不能证明的命题
猜想 5.1（符号死循环吸引域存在性）
陈述： 设 (X,d) 为完备度量空间，T:X\to X 连续且具备充分表达能力。则 T 的定义域内存在非空符号死循环吸引域。
状态：不能证明。
原因：
1. “充分表达能力”未形式化。
2. 一般连续算子不一定有吸引子。
3. 存在反例：T(x)=x+1 在 \mathbb{R} 上无不动点，更无吸引子。
4. 需要额外条件（如紧性、耗散性）才能保证吸引子存在。
诚实声明： 本猜想一般情形不成立。需加条件：X 紧、T 耗散、T 有界。在这些条件下，吸引子存在，但“符号死循环”需要额外定义全局目标。因此本猜想不能作为一般命题证明。
---
猜想 5.2（对称吸引盆测度猜想）
陈述： 带对称约束的连续优化问题中，高对称构型对应的临界点，其吸引盆拥有更大勒贝格测度。
状态：不能证明。
原因：
1. 吸引盆测度与对称性的关系没有一般定理。
2. 存在反例：某些系统中低对称构型吸引盆更大。
3. 需要具体系统具体分析。
诚实声明： 本猜想在特定系统（如 Thomson 问题小 N）可能成立，但一般情形不能证明。
---
猜想 5.3（李雅普诺夫—不可判定性对应）
陈述： K(\mathcal{S}) 内部复杂度分层可用李雅普诺夫谱作为定量指标。
状态：不能证明。
原因：
1. 不可判定性是静态逻辑属性，李雅普诺夫指数是动态行为。
2. 两者之间的桥没有建立。
3. 从形式命题到推演轨道的良定义映射不存在。
4. 李雅普诺夫谱对解释映射 \Pi 的稳定性未证明。
5. 逻辑发散与数值发散无法区分。
诚实声明： 这是一个研究纲领，不是猜想。它给出了方向，但核心问题全部开放。不能证明，也不假装能证明。
---
猜想 5.4（对称临界点陷阱猜想）
陈述： 对一般 Thomson 问题，高对称临界点不一定是全局极小。
状态：部分可证，一般情形不能证。
部分证明：
对 N=11，定理3.8已给出数值观察：U(25^\circ)<U(35.26^\circ)。这证明在 N=11 时，高对称临界点不是全局极小。
一般情形： 对任意 N，高对称临界点是否为全局极小，是开放问题。不能证明。
---
6 总表
命题 状态 说明
定理3.1 符号死循环判定 严格证明 改写版有内容
推论3.2 无外部校验不可区分 严格证明 可计算性理论
定理3.3 推演漂移存在性 严格证明 构造性例子
定理3.4 压缩映射信息衰减 严格证明 压缩映射标准结果
定理3.5 Pareto 前沿存在性 严格证明 Zorn 引理
定理3.6 路径依赖例子 严格证明 显式构造
定理3.7 两主体互检 严格证明 依赖独立性假设
定理3.8 区间算术误差界 严格证明 需实际计算
部分定理4.1 漂移概率单调性 部分证明 缺遍历理论
部分定理4.2 多主体收敛性 部分证明 缺收敛条件
猜想5.1 符号死循环吸引域 不能证明 一般情形不成立
猜想5.2 对称吸引盆测度 不能证明 无反例也无证明
猜想5.3 李雅普诺夫—不可判定性 不能证明 研究纲领
猜想5.4 对称临界点陷阱 部分可证 N=11 可证，一般开放
---
7 结论
能证的
1. 符号死循环判定定理；
2. 无外部校验不可区分；
3. 推演漂移存在性；
4. 压缩映射信息衰减；
5. Pareto 前沿存在性；
6. 路径依赖显式例子；
7. 两主体互检降低错误率；
8. 区间算术误差界。
部分证的
1. 漂移概率单调性；
2. 多主体交互收敛性。
不能证的
1. 符号死循环吸引域存在性（一般情形不成立）；
2. 对称吸引盆测度猜想（无反例也无证明）；
3. 李雅普诺夫—不可判定性对应（研究纲领）；
4. 对称临界点陷阱猜想（一般情形开放）。
最终声明
能证的证了，不能证的不假装证。
数学的诚实不在于声称解决一切，而在于明确边界。
本文的贡献是：
1. 把原有命题分层：定理、部分定理、猜想、研究纲领；
2. 给出能证部分的严格证明；
3. 明确不能证部分的原因；
4. 不把猜想伪装成定理。
---
附录 A：11电荷构型势能 U(\varphi) 完整展开
单位球面，11个电荷。点位清单：
· P_N：北极 (0,0,1)
· P_S：南极 (0,0,-1)
· N_0,N_1,N_2：纬度 \varphi，经度 0,2\pi/3,4\pi/3
· S_0,S_1,S_2：纬度 -\varphi，经度 \pi/3,\pi,5\pi/3
· E_0,E_1,E_2：赤道，经度 \pi/6,5\pi/6,3\pi/2
纬度 \varphi 使用弧度。笛卡尔坐标：
x=\cos\varphi\cos\lambda,\quad y=\cos\varphi\sin\lambda,\quad z=\sin\varphi
两点极角间隔 \theta，欧氏距离：
r=2\sin(\theta/2),\qquad U_{pair}=1/r
两点球面夹角公式：
\cos\theta=\sin\varphi_A\sin\varphi_B+\cos\varphi_A\cos\varphi_B\cos(\lambda_A-\lambda_B)
U_{AB}=\frac{1}{2\sin(\theta/2)}
全部 15 分项
1. 极—极（P_N,P_S）：
\theta=\pi,\quad U=0.5
2. 极—北纬（P_N 与 N_0,N_1,N_2，共3对）：
\theta=\pi/2-\varphi,\quad U=\frac{1}{2\sin(\pi/4-\varphi/2)}
乘以3。
3. 极—南纬（P_N 与 S_0,S_1,S_2，共3对）：
\theta=\pi/2+\varphi,\quad U=\frac{1}{2\sin(\pi/4+\varphi/2)}
乘以3。
4. 极—赤道（P_N 与 E_0,E_1,E_2，共3对）：
\theta=\pi/2,\quad U=1/\sqrt{2}
乘以3。
5. 南极—北纬（P_S 与 N_0,N_1,N_2，共3对）：同第3项，乘以3。
6. 南极—南纬（P_S 与 S_0,S_1,S_2，共3对）：同第2项，乘以3。
7. 南极—赤道（P_S 与 E_0,E_1,E_2，共3对）：同第4项，乘以3。
8. 北纬内部（N_0,N_1,N_2 两两，3对）：
经度差 2\pi/3，同纬度 \varphi：
\cos\theta=\sin^2\varphi-\frac{1}{2}\cos^2\varphi
9. 南纬内部（S_0,S_1,S_2 两两，3对）：与第8项完全对称。
10. 赤道内部（E_0,E_1,E_2 两两，3对）：
赤道，经度差 2\pi/3：
\cos\theta=-1/2,\quad \theta=2\pi/3
11. 北纬↔南纬（N_i 与 S_j，9对）：
经度差：\pi/3,\pi,5\pi/3，分三类，各3组：
\cos\theta=-\sin^2\varphi+\cos^2\varphi\cos(\Delta\lambda)
其中 \Delta\lambda\in\{\pi/3,\pi,5\pi/3\}。
12. 北纬↔赤道（N_i 与 E_j，9对）：
经度差：\pi/6,5\pi/6,3\pi/2 等，分三类：
\cos\theta=\cos\varphi\cos(\Delta\lambda)
13. 南纬↔赤道（S_i 与 E_j，9对）：同第12项。
总势能表达式
\begin{aligned}
U(\varphi)
&=U(P_N,P_S) \\
&+\sum_{k=0}^2 U(P_N,N_k)+\sum_{k=0}^2 U(P_N,S_k)+\sum_{k=0}^2 U(P_N,E_k) \\
&+\sum_{k=0}^2 U(P_S,N_k)+\sum_{k=0}^2 U(P_S,S_k)+\sum_{k=0}^2 U(P_S,E_k) \\
&+\sum_{i<j}U(N_i,N_j)+\sum_{i<j}U(S_i,S_j)+\sum_{i<j}U(E_i,E_j) \\
&+\sum_{i=0}^2\sum_{j=0}^2 U(N_i,S_j)+\sum_{i=0}^2\sum_{j=0}^2 U(N_i,E_j)+\sum_{i=0}^2\sum_{j=0}^2 U(S_i,E_j).
\end{aligned}
数值验证代码（Python）
```python
import numpy as np
def sphere_angle(phiA, lamA, phiB, lamB):
cos_theta = (np.sin(phiA)*np.sin(phiB)
+ np.cos(phiA)*np.cos(phiB)*np.cos(lamA - lamB))
cos_theta = np.clip(cos_theta, -1.0, 1.0)
return np.arccos(cos_theta)
def pair_potential(phiA, lamA, phiB, lamB):
theta = sphere_angle(phiA, lamA, phiB, lamB)
if theta < 1e-12:
return 0.0
return 1.0 / (2.0 * np.sin(theta / 2.0))
def total_potential(phi):
points = []
points.append((np.pi/2, 0.0)) # P_N
points.append((-np.pi/2, 0.0)) # P_S
for lam in [0.0, 2*np.pi/3, 4*np.pi/3]:
points.append((phi, lam)) # N_0,N_1,N_2
for lam in [np.pi/3, np.pi, 5*np.pi/3]:
points.append((-phi, lam)) # S_0,S_1,S_2
for lam in [np.pi/6, 5*np.pi/6, 3*np.pi/2]:
points.append((0.0, lam)) # E_0,E_1,E_2
U = 0.0
n = len(points)
for i in range(n):
for j in range(i+1, n):
phiA, lamA = points[i]
phiB, lamB = points[j]
U += pair_potential(phiA, lamA, phiB, lamB)
return U
if __name__ == "__main__":
phi_s = np.arctan(np.sqrt(2)) # ≈35.26°
phi_g = np.deg2rad(25.0)
U_s = total_potential(phi_s)
U_g = total_potential(phi_g)
print(f"phi_s = {np.rad2deg(phi_s):.4f} deg, U = {U_s:.10f}")
print(f"phi_g = {np.rad2deg(phi_g):.4f} deg, U = {U_g:.10f}")
print(f"U(phi_g) < U(phi_s): {U_g < U_s}")
```
---
附录 B：命题逻辑证明检查器（Python）
代码用途：实现外部验证器 O，逐行检查 A1/A2/A3 与 MP，给出 accept/reject/unknown。
```python
import re
from typing import List, Tuple
def tokenize(s: str) -> List[str]:
s = s.replace(" ", "")
tokens, i = [], 0
while i < len(s):
c = s[i]
if c in "()":
tokens.append(c); i += 1
elif c == "¬":
tokens.append("¬"); i += 1
elif c == "-" and i + 1 < len(s) and s[i+1] == ">":
tokens.append("→"); i += 2
elif c.isalpha():
tokens.append(c); i += 1
else:
raise ValueError(f"非法字符: {c}")
return tokens
def parse(tokens: List[str]):
pos = 0
def peek(): return tokens[pos] if pos < len(tokens) else None
def consume(expected=None):
nonlocal pos
tok = peek()
if tok is None: raise ValueError("公式不完整")
if expected and tok != expected: raise ValueError(f"期望 {expected}，得到 {tok}")
pos += 1; return tok
def parse_imp():
left = parse_not()
if peek() == "→":
consume("→"); return ("→", left, parse_imp())
return left
def parse_not():
if peek() == "¬":
consume("¬"); return ("¬", parse_not())
return parse_atom()
def parse_atom():
tok = peek()
if tok == "(":
consume("("); node = parse_imp(); consume(")"); return node
if tok and tok.isalpha():
consume(); return ("atom", tok)
raise ValueError(f"非法片段: {tok}")
node = parse_imp()
if pos != len(tokens): raise ValueError(f"解析未到末尾: {tokens[pos:]}")
return node
def parse_formula(s: str): return parse(tokenize(s))
def to_str(node) -> str:
if node[0] == "atom": return node[1]
if node[0] == "¬": return f"¬{to_str(node[1])}"
if node[0] == "→": return f"({to_str(node[1])}→{to_str(node[2])})"
raise ValueError("未知节点")
def match(pattern, formula, subst: dict) -> bool:
if pattern[0] == "atom":
name = pattern[1]
if name in subst: return subst[name] == formula
subst[name] = formula; return True
if pattern[0] == "¬":
return formula[0] == "¬" and match(pattern[1], formula[1], subst)
if pattern[0] == "→":
return (formula[0] == "→"
and match(pattern[1], formula[1], subst)
and match(pattern[2], formula[2], subst))
return False
def pat_A1(): return ("→", ("atom", "phi"), ("→", ("atom", "psi"), ("atom", "phi")))
def pat_A2():
phi, psi, chi = ("atom", "phi"), ("atom", "psi"), ("atom", "chi")
return ("→", ("→", phi, ("→", psi, chi)), ("→", ("→", phi, psi), ("→", phi, chi)))
def pat_A3():
phi, psi = ("atom", "phi"), ("atom", "psi")
return ("→", ("→", ("¬", phi), ("¬", psi)), ("→", psi, phi))
def is_axiom_instance(formula):
for name, pat in [("A1", pat_A1()), ("A2", pat_A2()), ("A3", pat_A3())]:
subst = {}
if match(pat, formula, subst): return name
return None
def check_proof(lines: List[str]) -> Tuple[str, List[str]]:
report, parsed_lines = [], []
for idx, raw in enumerate(lines, start=1):
if "|" not in raw:
return "unknown", [f"第 {idx} 行缺少依据分隔符 |"]
formula_str, reason = raw.split("|", 1)
formula_str, reason = formula_str.strip(), reason.strip()
try:
formula = parse_formula(formula_str)
except Exception as e:
return "unknown", [f"第 {idx} 行公式解析失败: {e}"]
parsed_lines.append((formula, formula_str, reason))
for idx, (formula, formula_str, reason) in enumerate(parsed_lines, start=1):
ru = reason.upper()
if ru in ("A1", "A2", "A3"):
hit = is_axiom_instance(formula)
if hit != ru:
return "reject", [f"第 {idx} 行非法: {formula_str} 不是 {ru} 的实例"
+ (f"，实际匹配 {hit}" if hit else "")]
report.append(f"第 {idx} 行合法: {ru} 实例"); continue
if ru.startswith("MP"):
m = re.match(r"MP\s*(\d+)\s*,\s*(\d+)", reason, re.IGNORECASE)
if not m:
return "reject", [f"第 {idx} 行非法: MP 依据格式错误: {reason}"]
i, j = int(m.group(1)), int(m.group(2))
if not (1 <= i < idx and 1 <= j < idx):
return "reject", [f"第 {idx} 行非法: MP 引用行号 {i},{j} 不早于当前行"]
f_i, f_j = parsed_lines[i-1][0], parsed_lines[j-1][0]
if f_j[0] == "→" and f_i == f_j[1]:
expected = f_j[2]
elif f_i[0] == "→" and f_j == f_i[1]:
expected = f_i[2]
else:
return "reject", [f"第 {idx} 行非法: MP {i},{j} 无法推出 {formula_str}。"
f"第{i}行={parsed_lines[i-1][1]}，第{j}行={parsed_lines[j-1][1]}"]
if expected != formula:
return "reject", [f"第 {idx} 行非法: MP {i},{j} 应推出 {to_str(expected)}，"
f"但写的是 {formula_str}"]
report.append(f"第 {idx} 行合法: MP {i},{j}"); continue
return "reject", [f"第 {idx} 行非法: 未知依据 {reason}"]
return "accept", report
if __name__ == "__main__":
proofs = {
"证明1（合法）": [
"P -> ((P -> P) -> P) | A1",
"(P -> ((P -> P) -> P)) -> ((P -> (P -> P)) -> (P -> P)) | A2",
"(P -> (P -> P)) -> (P -> P) | MP 1,2",
"P -> (P -> P) | A1",
"P -> P | MP 4,3",
],
"证明2（非法）": [
"P -> (P -> P) | A1",
"(P -> (P -> P)) -> ((P -> P) -> P) | A2",
"(P -> P) -> P | MP 1,2",
"P -> P | ???",
],
}
for name, lines in proofs.items():
label, rep = check_proof(lines)
print(f"===== {name} =====")
print("结果:", label)
for r in rep: print(" " + r)
print()
```
---
守拙同观·魏嵬·天水
2026年10月3日
#迭代推演 #吸引子陷阱 #魏嵬AI闭环哲学
