# 形式證明不等於過程證明：Theoremhood 與 Process Completeness

**系列：形式封閉與過程完備：AI 數學證明的下一步問題**  
**Paper 01**  
**作者：Neo.K / EveMissLab Research Series**  
**版本：v0.1 — 2026-09-11**

**機構：** EveMissLab／一言諾科技有限公司  
**日期：** 2026-09-11  

---

## 摘要

現代形式化數學通常把「證明完成」理解為：在一套明確的形式系統中，某個命題具有可驗證的 proof term，且該 proof term 能通過 kernel checking。這種標準極其重要，並且大幅降低了紙面證明中的遺漏、符號錯置與局部推理錯誤。然而，當研究問題本身涉及動態過程、逐步生成、無限階構造、極限轉移、對角實現、存在性選擇或跨尺度演化時，單純的 theoremhood 並不自動等價於 process completeness。

本文提出一個基本區分：

$$
\boxed{
\text{Theorem Closure}
\neq
\text{Process Completeness}
}
$$

前者回答「結論是否能從形式前提推出」；後者則要求進一步回答「每一個狀態是否真的由上一個狀態沿合法箭頭生成」、「有限階段是否形成同一條可延續路徑」、「極限物件是否來自原過程本身，而不是由新的 completion operator 事後實現」，以及「存在性證明是否對應某種可構造或可計算的生成程序」。

本文建立五層審計框架：Kernel Validity、Specification Validity、Arrow Validity、Trace Validity 與 Computational Realizability，並提出 Process-Complete Proof 的初步形式定義。本文的核心目的不是否定形式化證明，而是指出：對某些問題而言，形式化證明是必要條件，但仍不是全部研究義務。若未把「下一步為什麼是下一步」正式納入規格，proof assistant 可以完全正確地驗證一個仍具有過程語義缺口的命題。

---

## 關鍵詞

形式化證明、Lean、過程完備性、箭頭合法性、trajectory、same-parent path、存在性證明、對角化、極限、Classical.choice、可計算性、AI 數學、proof ontology

---

# 1. 問題：一個被證明的命題，是否已經等於一個被完成的過程？

假設某個形式系統證明：

$$
\Gamma \vdash T.
$$

在標準 proof-theoretic 意義下，只要 proof term 可由可信 kernel 驗證，則 $T$ 是相對於 $\Gamma$ 的定理。

這個判準非常清楚：

$$
\operatorname{ValidProof}(\Gamma,T)=1.
$$

然而，當 $T$ 描述的是一個動態過程，例如：

$$
S_0\to S_1\to S_2\to\cdots,
$$

問題就不再只有：

$$
\Gamma\vdash T
$$

是否成立。

還存在另一組問題：

$$
S_n\to S_{n+1}
$$

究竟是哪一種箭頭？

是否存在同一個生成規則？

是否所有 $S_n$ 屬於同一條 parent-consistent path？

是否最後的極限物件真的是這條 path 的極限？

是否某個「存在」只是形式系統中可選取，而不是可以由過程實際生成？

因此，本文首先提出：

> **定理成立與過程完成是兩個不同層級的判斷。**

---

# 2. 第一個區分：Theorem Closure

定義一個形式理論：

$$
\mathcal T=(\mathcal L,\mathcal A,\mathcal R),
$$

其中：

- $\mathcal L$ 是語言；
- $\mathcal A$ 是公理與定義；
- $\mathcal R$ 是合法推理規則。

若命題 $P$ 存在有限 proof object $\pi$，使：

$$
\operatorname{Check}_{\mathcal T}(\pi,P)=\mathrm{true},
$$

則稱 $P$ 在 $\mathcal T$ 中達成 **Theorem Closure**。

可寫成：

$$
\operatorname{TC}_{\mathcal T}(P)=1.
$$

這正是 Lean、Coq、Isabelle 類系統最核心、也最可靠的能力。

重要的是，Theorem Closure 所要求的通常只是一個有限 proof representation。

例如數學歸納法可以證明：

$$
\forall n\in\mathbb N,\;P(n),
$$

但 kernel 並不需要逐一執行：

$$
P(0),P(1),P(2),P(3),\ldots
$$

直到某個「無限終點」。

它只需要驗證有限規則：

$$
P(0)
$$

以及：

$$
\forall n,\quad P(n)\Rightarrow P(n+1).
$$

因此：

$$
\text{finite proof term}
\Rightarrow
\text{statement over infinitely many instances}.
$$

這完全是形式數學的正常能力。

問題在於：如果研究者真正關心的是「那些 instance 是否構成同一條生成路徑」，那麼這個問題並沒有自動被回答。

---

# 3. 第二個區分：Arrow Validity

考慮狀態空間：

$$
\mathcal S.
$$

對任意兩個狀態：

$$
S,S'\in\mathcal S,
$$

我們引入箭頭：

$$
S\xrightarrow{\alpha}S'.
$$

普通存在性證明可能只要求：

$$
\forall n,\quad \exists S_{n+1}\;P(S_n,S_{n+1}).
$$

但如果研究問題具有過程語義，我們需要更強的要求：

$$
\operatorname{Admissible}(S_n,S_{n+1},\alpha_n).
$$

這表示： $S_{n+1}$ 不是任意滿足某些條件的 witness，而是可以由 $S_n$ 經過被允許的 transition $\alpha_n$ 生成。

因此定義：

$$
\operatorname{AV}(S_n,S_{n+1})
=
1
$$

當且僅當存在一個合法箭頭 $\alpha_n$，使：

$$
S_n\xrightarrow{\alpha_n}S_{n+1}.
$$

這與：

$$
\exists S_{n+1}\;P(S_{n+1})
$$

具有本質差異。

後者只回答「下一個狀態存在」。

前者回答：

> **為什麼它是這一個狀態的下一步？**

---

# 4. Same-Parent Path：存在很多節點，不代表存在一條路徑

令：

$$
L_n
$$

表示第 $n$ 層所有合法狀態集合。

假設：

$$
L_n\neq\varnothing
$$

對所有 $n$ 成立。

這並不自動推出存在：

$$
(S_0,S_1,S_2,\ldots)
$$

使：

$$
S_n\in L_n
$$

且：

$$
S_n\to S_{n+1}
$$

對每個 $n$ 都成立。

也就是：

$$
\forall n,\quad L_n\neq\varnothing
$$

不等價於：

$$
\exists (S_n)_{n\in\mathbb N},
\quad
\forall n,\;
S_n\in L_n
\land
S_n\to S_{n+1}.
$$

差異就在 compatibility。

我們稱後者為 **Same-Parent Path Condition**。

形式上：

$$
\operatorname{SPP}((S_n))
:=
\forall n,\;
\operatorname{ParentCompatible}(S_n,S_{n+1}).
$$

因此：

$$
\boxed{
\text{State existence}
\neq
\text{Path existence}
}
$$

進一步：

$$
\boxed{
\text{Path existence}
\neq
\text{Path generation}
}
$$

因為即使 classical choice 幫助我們選出一條序列，也不表示存在可執行的生成規則：

$$
S_{n+1}=F(S_n).
$$

---

# 5. 第三個區分：Trace Validity

一個真正的過程不只是節點集合，而是 trace：

$$
\tau:\mathbb N\to\mathcal S.
$$

定義：

$$
\tau(0)=S_0
$$

以及：

$$
\forall n,\quad
\operatorname{Step}(\tau(n),\tau(n+1)).
$$

若以上成立，稱 $\tau$ 是合法 trace。

也就是：

$$
\operatorname{TV}(\tau)=1.
$$

因此一個過程性 theorem 若只證：

$$
\forall n,\quad \exists S_n\;P_n(S_n),
$$

它還沒有證：

$$
\exists\tau:\mathbb N\to\mathcal S,
\quad
\operatorname{TV}(\tau)=1.
$$

這裡可看見一個常見語義壓縮：

$$
\forall n\exists S_n
$$

在形式邏輯中可以藉由選擇原理得到一個 total function。

但：

$$
\exists\tau
$$

仍不等於：

$$
\tau(n+1)
$$

是由：

$$
\tau(n)
$$

內生產生。

因此本文區分：

$$
\text{Choice Trace}
$$

與：

$$
\text{Generated Trace}.
$$

---

# 6. 第四個區分：Process Completeness

我們現在可以提出初步定義。

對一個宣稱描述過程的證明 $\Pi$，若其結論依賴狀態鏈：

$$
S_0,S_1,\ldots
$$

則稱 $\Pi$ 具有 **Process Completeness**，至少需要：

$$
\mathrm{PC}_1:
\quad
S_0\text{ 被合法初始化};
$$

$$
\mathrm{PC}_2:
\quad
\forall n,\;
S_n\to S_{n+1}
\text{ 的箭頭合法};
$$

$$
\mathrm{PC}_3:
\quad
(S_n)
\text{ 為 same-parent trace};
$$

$$
\mathrm{PC}_4:
\quad
\text{若使用極限 }S_*,\text{ 必須證明 }S_*
\text{ 來自該 trace 的合法 completion};
$$

$$
\mathrm{PC}_5:
\quad
任何在極限處使用的性質轉移皆有明確 transfer theorem。
$$

因此：

$$
\operatorname{PC}(\Pi)=1
$$

需要的不只是 theorem conclusion，而是 proof graph 中所有關鍵生成箭頭都有語義閉合。

---

# 7. Completion Operator：最容易被忽略的額外箭頭

假設我們已有：

$$
S_0,S_1,S_2,\ldots
$$

接著證明突然定義：

$$
S_*:=\mathcal C(\{S_n\}_{n\in\mathbb N}),
$$

其中 $\mathcal C$ 可能是：

- 極限；
- 對角化；
- Borel realization；
- completion；
- compactness extraction；
- weak limit；
- subsequence selection；
- classical choice；
- gluing；
- extension theorem。

這時證明圖實際上不是：

$$
S_0\to S_1\to S_2\to\cdots\to S_*.
$$

而是：

$$
\{S_n\}_{n\in\mathbb N}
\xrightarrow{\mathcal C}
S_*.
$$

因此 $\mathcal C$ 是一個新的 proof-level operator。

它必須獨立接受審計。

我們定義：

$$
\operatorname{CO}(\mathcal C)
$$

為 Completion Operator。

核心問題包括：

$$
\operatorname{Domain}(\mathcal C)?
$$

$$
\operatorname{Compatibility}(\mathcal C)?
$$

$$
\operatorname{Preservation}(\mathcal C)?
$$

$$
\operatorname{Uniqueness}(\mathcal C)?
$$

$$
\operatorname{Computability}(\mathcal C)?
$$

以及最關鍵的：

$$
\boxed{
\mathcal C(\{S_n\})
\text{ 是否仍屬於原過程的語義？}
}
$$

一個 completion operator 可以在古典分析中完全合法，但仍不是原生成機制的一步。

這正是：

$$
\boxed{
\text{Logical completion}
\neq
\text{process continuation}
}
$$

---

# 8. 第五個區分：Computational Realizability

即使：

$$
\exists\tau:\mathbb N\to\mathcal S
$$

且：

$$
\operatorname{TV}(\tau)=1,
$$

仍然不代表 $\tau$ 可計算。

若我們希望過程真正具有演算法意義，需要存在：

$$
F:\mathcal S\to\mathcal S
$$

使：

$$
\tau(n+1)=F(\tau(n)).
$$

並且 $F$ 在有限資源下可求值。

因此我們引入：

$$
\operatorname{CR}(F)=1
$$

表示 $F$ 具 Computational Realizability。

更進一步，如果存在極限：

$$
\tau(n)\to S_*,
$$

若要把「接近極限」轉成可操作計算，通常還需要 modulus：

$$
\mu:\mathbb Q_{>0}\to\mathbb N,
$$

使：

$$
n\ge\mu(\varepsilon)
\Rightarrow
d(\tau(n),S_*)<\varepsilon.
$$

若 $\mu$ 可計算，極限才具有更強的 constructive content。

因此：

$$
\text{existence}
\neq
\text{effective existence}.
$$

---

# 9. 五層證明審計框架

本文提出以下五層框架。

## Layer 1 — Kernel Validity

問題：

$$
\Gamma\vdash T?
$$

檢查 proof term 是否能由可信 kernel 通過。

---

## Layer 2 — Specification Validity

問題：

$$
T
\stackrel{?}{=}
\text{真正想回答的問題}.
$$

這一層防止：

$$
\text{proof correct}
+
\text{problem encoded too weakly}.
$$

---

## Layer 3 — Arrow Validity

問題：

$$
S_n\to S_{n+1}
$$

是否具有合法 process semantics。

不能只證：

$$
\exists S_{n+1}.
$$

---

## Layer 4 — Trace Validity

問題：

$$
\exists\tau
$$

是否真的是 same-parent path。

若：

$$
\tau(n)
$$

與：

$$
\tau(n+1)
$$

只是分別被選出，則仍需要 compatibility proof。

---

## Layer 5 — Computational Realizability

問題：

$$
\tau
$$

或：

$$
\operatorname{Step}
$$

是否可以被演算法實現。

這一層不一定是所有數學 theorem 的必要條件，但對宣稱「過程」「生成」「演化」「模擬」的 theorem 特別重要。

---

# 10. 一個最小反例模式

考慮：

$$
\forall n\in\mathbb N,
\quad
\exists x_n\in X_n.
$$

形式上，每一層都有 witness。

現在加入：

$$
R_n\subseteq X_n\times X_{n+1}.
$$

若 theorem 需要的是：

$$
\exists (x_n),
\quad
\forall n,\;
(x_n,x_{n+1})\in R_n,
$$

那麼：

$$
\forall n,\quad X_n\neq\varnothing
$$

顯然不夠。

甚至：

$$
\forall n,\forall x_n\in X_n,
\quad
\exists x_{n+1}\in X_{n+1},
\quad
(x_n,x_{n+1})\in R_n
$$

雖然能在 choice 下構造 path，仍不一定給出 computable transition。

因此至少存在三種強度：

$$
E_1:
\quad
\forall n\exists x_n,
$$

$$
E_2:
\quad
\exists (x_n)\forall n\;R_n(x_n,x_{n+1}),
$$

$$
E_3:
\quad
\exists F\;
\forall n,\;
x_{n+1}=F(x_n).
$$

通常：

$$
E_3\Rightarrow E_2\Rightarrow E_1,
$$

但反方向不自動成立。

---

# 11. 「如果，所以，然後」真正的問題是什麼？

數學證明本來就必須包含大量：

$$
P\Rightarrow Q.
$$

所以「如果、所以、然後」本身完全不是缺陷。

真正需要審計的是：

> **每一個 implication 是否仍位於同一個問題域與同一個生成語義中？**

若：

$$
P_n\Rightarrow P_{n+1}
$$

是合法 successor theorem，則沒有問題。

若某一步突然變成：

$$
\{P_n\}_{n\in\mathbb N}
\Rightarrow
Q
$$

並且 $Q$ 透過一個新的 $\mathcal C$ 被實現，那麼必須標記：

$$
\boxed{
\text{這不是普通 successor arrow，而是 completion arrow。}
}
$$

形式證明系統可能會把兩者都表示成 function application。

但研究語義不能因此把它們視為同一種步驟。

---

# 12. Proof Assistant 的能力邊界不是「不夠嚴格」，而是「只驗你寫進去的規格」

這裡需要避免一個常見誤解。

如果 Lean 通過了一個 theorem，但 theorem 並未要求 process completeness，不能說 Lean「漏掉」了 process completeness。

Lean 的工作是：

$$
\operatorname{Check}(\text{formal specification}).
$$

不是：

$$
\operatorname{Infer}(\text{all unstated scientific obligations}).
$$

因此真正的問題是：

$$
\boxed{
\text{omitted semantic obligation}
}
$$

沒有被寫入 formal statement。

Proof assistant 無法驗證一個從未被形式化的 requirement。

所以未來形式化數學若要處理 process-sensitive theorem，必須把：

$$
\operatorname{Step},
\quad
\operatorname{Trace},
\quad
\operatorname{ParentCompatibility},
\quad
\operatorname{CompletionOperator},
\quad
\operatorname{TransferLaw}
$$

升格為一級形式物件。

---

# 13. AI 數學時代的新風險

當 AI theorem prover 越來越強，可能出現一個反直覺現象：

$$
\text{formal closure capability}\uparrow
$$

不一定自動推出：

$$
\text{problem ontology judgment}\uparrow.
$$

AI 可能非常擅長：

$$
\text{找到一條能封閉 theorem 的路}
$$

卻不一定主動追問：

$$
\text{這條 theorem 是否就是最值得證明的問題？}
$$

因此可能出現：

$$
\boxed{
\text{specification-minimal resolution}
}
$$

亦即：

在形式規格允許的範圍內，找到最容易被完整證明的合法路徑。

這不是錯。

但它可能比研究者原本口語上理解的「解掉整個問題」更窄。

因此未來 AI 數學系統不能只評估：

$$
\text{proof success rate}.
$$

還應評估：

$$
\text{semantic depth},
$$

$$
\text{arrow completeness},
$$

$$
\text{problem reconstruction ability},
$$

與：

$$
\text{claim scope discipline}.
$$

---

# 14. Process-Complete Theorem 的初步規格

本文提出一個初步 schema。

對任意動態 theorem：

$$
\mathfrak P
=
(S_0,\mathcal T,\mathcal I,\mathcal G),
$$

其中：

- $S_0$：初始狀態；
- $\mathcal T$：合法 transition relation；
- $\mathcal I$：需要維持的 invariants；
- $\mathcal G$：目標性質。

一個 process-complete proof 至少應證明：

$$
\exists\tau,
$$

使：

$$
\tau(0)=S_0,
$$

$$
\forall n,\quad
\mathcal T(\tau(n),\tau(n+1)),
$$

$$
\forall n,\quad
\mathcal I(\tau(n)),
$$

並且若：

$$
\tau\to S_*,
$$

則必須證：

$$
\operatorname{LegalCompletion}(\tau,S_*),
$$

以及：

$$
\mathcal G(S_*).
$$

若 theorem 宣稱演算法性，則再要求：

$$
\tau(n+1)=F(\tau(n))
$$

其中 $F$ 為可計算 transition。

因此：

$$
\boxed{
\text{Process-Complete Proof}
=
\text{Theorem Closure}
+
\text{Arrow Closure}
+
\text{Trace Closure}
+
\text{Completion Closure}
}
$$

在需要計算意義時，再加：

$$
+
\text{Computational Closure}.
$$

---

# 15. 核心命題

本文的核心命題可濃縮為四句。

第一：

$$
\boxed{
\text{A proof of existence is not automatically a proof of generation.}
}
$$

第二：

$$
\boxed{
\text{A family of valid finite stages is not automatically a completed path.}
}
$$

第三：

$$
\boxed{
\text{A legal completion operator is not automatically the next step of the original process.}
}
$$

第四：

$$
\boxed{
\text{Machine-checked theoremhood does not by itself establish process completeness.}
}
$$

這四句不否定形式化數學。

相反，它們要求更強的形式化。

---

# 16. 結論

形式化證明的成功，解決了數學史上一個極為重要的問題：我們終於可以把大量 proof checking 從人類信任轉移到機器 kernel。

但下一個問題已經出現：

> **當 theorem 本身描述一個過程時，我們究竟證明了命題，還是證明了過程？**

如果 proof 只說：

$$
\forall n\exists x_n,
$$

而研究問題實際需要：

$$
x_0\to x_1\to x_2\to\cdots,
$$

則兩者之間仍存在語義距離。

如果 finite corrections 最後透過新的 diagonal operator 被組成一個 smooth object，那麼我們必須區分：

$$
\text{realization}
$$

與：

$$
\text{trajectory completion}.
$$

如果 classical choice 產生一個 total function，則我們必須區分：

$$
\text{selected object}
$$

與：

$$
\text{generated object}.
$$

因此，未來高階形式數學與 AI theorem proving 的重要方向，不只是建立更多可驗證 theorem，而是建立：

$$
\boxed{
\text{Proof Systems That Can Audit Their Own Arrows.}
}
$$

也就是：不只問結論是否成立，還要問每一個「所以」究竟代表哪一種合法轉換。

---

# 17. 系列後續

本文只建立一般理論框架。

下一篇將集中處理：

## Paper 02 — 下一步到底為什麼是下一步：Arrow Legitimacy 與 Same-Parent Path

核心問題是：

$$
\boxed{
\text{What makes the next state genuinely the next state?}
}
$$

並進一步建立 successor legality、parent compatibility、branch consistency 與 path preservation 的形式模型。