# 證明助理中的形式陳述：逐層讀懂一個 Lean 陳述並區分「是陳述」與「已證明」

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-lean-formal-statement/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-lean-formal-statement-01 · production-20261019-adopted-96



## 目標與範圍

以源碼字串 s：`∀ (a b : Nat), a ≤ b → a < b + 1` 為教學對象，在一個明示固定但未實際執行的環境 E 中逐層說明：它的約束變數與型別、假設與結論、若 elaboration 成功應得到的核心項 S、為何 S 的型別會是 Prop、一個證明項必須建立什麼；再給出其數學內容的非正式證明，並以 s′：`∀ (a : Nat), a - 1 < a`（是 Prop 但為假）與 s″：`∀ (a : Int), a - 1 < a`（為真）對照。全程未執行 Lean，不宣稱任何內容可解析、可 elaboration、已編譯或已被 Lean 證明。

在 MKO 範圍內工作：陳述身分包含 Lean 版本、imports、名稱環境與 local context（假設 a1）；依使用者指示暫停 Lean，所以只做概念說明與手工型別分析，不產生任何 elaboration 或 kernel receipt（假設 a2）。所引用的 Lean 記號與型別規則以 citation_verified 標記；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- numeric_evaluation
- def_unfold


- G1 — 環境 E=(V,I,N,Γ)：V 是某個指定的 Lean 4 版本（應於恢復 Lean 工作時記入 receipt，本稿未釘選）；I 為除 Lean 4 core prelude 外沒有其他 imports；N 為該 prelude 所宣告的名稱；Γ 為空的 local context。四者都是陳述身分的一部分（MKO 假設 a1）。
- G2 — 本稿不執行 Lean（使用者指示；MKO 假設 a2）：沒有執行解析、elaboration、型別檢查或 kernel check。下文關於這些階段的每句話，要嘛是該階段必須建立什麼的定義，要嘛是以該階段成功為前提的手工分析。
- G3 — 源碼字串 s = `∀ (a b : Nat), a ≤ b → a < b + 1`。若要宣告定理，還需寫成 theorem t : s := p 並提供證明 p；本稿只討論冒號後的陳述部分。
- G4 — 對照字串 s′ = `∀ (a : Nat), a - 1 < a` 與 s″ = `∀ (a : Int), a - 1 < a`，在同一 E 中閱讀。


- E=(V,I,N,\Gamma) — 環境：Lean 版本、imports、名稱環境、local context
- s — 源碼字串（尚未解析的文字）
- S — 若 elaboration 成功所得的核心項
- \Gamma\vdash S:\mathrm{Prop} — 在 Γ 中 S 的型別是 Prop
- p — S 的候選證明項
- \mathsf{Elab},\ \mathsf{Kernel} — elaboration 與 kernel check 兩個階段
- \mathrm{Nat},\ \mathrm{Int} — Lean 的自然數型別與整數型別





## 規則與來源


- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- imp_intro · prerequisite — →引入（釋放假設）：若在暫時假設 P 的作用域中推出 Q，則得到 P⇒Q；此後 P 不再可當作已知使用。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_lean_formal_statement_def · cited — 在固定 Lean 版本、imports、名稱環境與 local context Γ 中，source syntax s 若成功 elaboration 為核心項 S，且 Γ⊢S:Prop，則 s 在該環境中表達一個形式陳述。陳述成立與存在已檢查證明項是分離狀態。 · mko-lean-formal-statement
- mko_proposition_def · cited — 命題 P 可以為真或為假；P 是命題不表示 P 已被證明為真。 · mko-proposition
- lean_stages · cited — Lean 4 分階段處理源碼：解析把文字變成語法樹；elaboration 把語法變成核心項，並解析名稱、記號、隱式參數與 type-class instance，可能失敗；型別檢查推得核心項的型別；宣告定理時，kernel 檢查所提供的證明項具有所宣告的型別。前一階段成功不保證後一階段成功。 · Lean Language Reference, Elaboration and Compilation, Sections 2.1-2.3
- lean_core_notation · cited — 在 Lean 4 core 中，a ≤ b 是 LE.le a b 的記號，a < b 是 LT.lt a b，a + b 是 HAdd.hAdd a b，a - b 是 HSub.hSub a b，數字 1 是 OfNat.ofNat 1；LE.le 與 LT.lt 的型別是 α → α → Prop。+ 的結合力強於 ≤ 與 <，兩者又強於 →；→ 向右結合；∀ 的作用域延伸到最右；(a b : Nat) 宣告兩個型別為 Nat 的約束變數。core prelude 為 Nat 與 Int 提供這些類別的 instance。 · Lean 4 v4.30.0 Init/Notation.lean; Lean Language Reference Basic Classes; Init.Prelude API
- prop_formation · cited — Lean 型別論的規則：(i) 若 Γ⊢A:Prop 且 Γ⊢B:Prop，則 Γ⊢(A→B):Prop；(ii) 若 Γ⊢α:Sort u 且 Γ,x:α⊢B:Prop，則 Γ⊢(∀x:α, B):Prop（Prop 的非直謂性）；Nat : Type 與 Int : Type，其中 Type = Sort 1。 · Theorem Proving in Lean 4, Chapters 3 and 4, Sections 3.1 and 4.1
- curry_howard · cited — 命題即型別：∀x:α, B 的證明是把每個 x:α 送到 B 的證明的函數；A→B 的證明是把 A 的證明送到 B 的證明的函數；p : S 表示 p 是型別為 S 的項。 · Theorem Proving in Lean 4, Sections 3.1 and 4.1
- nat_trunc_sub · cited — 在 Lean 4 core 中，Nat 上的減法是截斷減法：a≤b 時 a−b=0，否則為通常的差；特別地 0−1=0。Int 上的減法是通常的環減法。 · Lean 4 Init.Prelude API, Nat.sub; Lean Language Reference, Integers, Int.sub
- L_main · lemma — 對所有自然數 a、b：若 a≤b，則 a<b+1。





## 逐步主鏈

S01 · definition操作前

s,\ E

操作後

E=(V,I,N,\Gamma),\quad \Gamma=\varnothing

條件：\text{Lean not run (G2)}

規則：def_intro · 依賴：G1, G2

葉節點依據：def_intro + mko_lean_formal_statement_def

先把環境寫成四元組並命名。MKO 假設 a1 說版本、imports、已宣告名稱與 local context 都屬於陳述身分，所以任何關於 s 的判斷都必須附上 E。G2 記錄：這個四元組只在紙上固定，沒有呼叫任何工具鏈。



S02 · definition操作前

s

操作後

\mathsf{Parse}(s)\ ;\ \mathsf{Elab}(s)=S\ ;\ \Gamma\vdash S:\mathrm{Prop}\ ;\ \Gamma\vdash p:S\ ;\ \mathsf{Kernel}(p,S)

條件：無

規則：lean_stages · 依賴：S01, G3

葉節點依據：lean_stages + def_intro

為五個狀態命名：s 被解析；s elaboration 成核心項 S；S 的型別是 Prop；存在證明項 p:S；p 通過 kernel check。後面的狀態以前面的狀態為前提，但前面的狀態都不蘊含後面的狀態。MKO 的誤解正是把這幾個狀態合成一件事。本稿開始時五個狀態都是「未執行」。



S03 · implies操作前

s=\texttt{∀ (a b : Nat), a ≤ b → a < b + 1}

操作後

\forall a:\mathrm{Nat},\ \forall b:\mathrm{Nat},\ \bigl((a\le b)\to(a<(b+1))\bigr)

條件：\text{notation and precedence of E as cited}

規則：lean_core_notation · 依賴：S02, G3

葉節點依據：lean_core_notation

依引用的記號與優先序慣例手工讀出結構：(a b : Nat) 是兩個巢狀的全稱約束；∀ 延伸到字串結尾；+ 比 < 結合得緊，所以 a < b + 1 是 a<(b+1)；≤ 與 < 比 → 結合得緊，所以 → 的兩邊是 a≤b 與 a<b+1。讀出的意思：對所有自然數 a、b，若 a≤b 則 a<b+1。這是按慣例的人工閱讀，不是執行解析器的結果（G2）。



S04 · implies操作前

\forall a\,b:\mathrm{Nat},\ a\le b\to a<b+1

操作後

S=\forall a\,b:\mathrm{Nat},\ \mathrm{LE.le}\,a\,b\to\mathrm{LT.lt}\,a\,(\mathrm{HAdd.hAdd}\,b\,(\mathrm{OfNat.ofNat}\,1))

條件：\mathsf{Elab}(s)\ \text{succeeds (not run)}

規則：lean_core_notation · 依賴：S03

葉節點依據：lean_core_notation + lean_stages

說明 elaboration 若成功必須產生什麼：把每個記號換成其常數，並補上隱式型別參數 Nat 與 instance 參數（LE Nat、LT Nat、HAdd Nat Nat Nat、OfNat Nat 1）；顯示的項省略了這些隱式參數。這是對 elaboration 任務的描述；它是否成功、instance 的確切名稱，本稿都沒有檢查。



S05 · theorem_application操作前

S

操作後

\Gamma\vdash S:\mathrm{Prop}\quad(\text{conditional on}\ \mathsf{Elab}(s)=S)

條件：\mathsf{Elab}(s)=S

規則：prop_formation · 依賴：S04

葉節點依據：prop_formation + lean_core_notation

以 S04 的形狀為前提，用型別形成規則逐層推得 S 的型別是 Prop：先是兩個原子命題（S05.1），再是蘊含（S05.2），最後是兩層全稱（S05.3）。這是手工型別分析，不是型別檢查器的輸出。



S06 · implies操作前

\mathsf{Elab}(s)=S\ \wedge\ \Gamma\vdash S:\mathrm{Prop}

操作後

s\ \text{expresses a formal statement in}\ E

條件：\mathsf{Elab}(s)=S\ \text{(not run)}

規則：mko_lean_formal_statement_def · 依賴：S05, S02

葉節點依據：mko_lean_formal_statement_def + lean_stages

套用 MKO 定義作為條件式：若 s 在 E 中 elaboration 為 S 且 Γ⊢S:Prop，則 s 在 E 中表達一個形式陳述。前件的型別部分已在 S05 以 elaboration 成功為前提手工得到；elaboration 本身沒有執行（G2）。因此記錄的狀態是：「預期在 E 中表達形式陳述；缺 elaboration receipt」。



S07 · definition操作前

\Gamma\vdash p:S

操作後

p=\lambda (a\,b:\mathrm{Nat})\,(h:a\le b).\ q,\quad a,b:\mathrm{Nat},\ h:a\le b\ \vdash\ q:a<b+1

條件：無

規則：curry_howard · 依賴：S04

葉節點依據：curry_howard

依命題即型別，S 的證明項是一個函數：接收任意 a、b : Nat 與假設 a≤b 的證明 h，回傳 a<b+1 的證明 q。約束變數 a、b 是資料，h 是假設；證明責任是：對任意 a、b 與 h，造出 a<b+1 的證明。這正是 S09 非正式證明的形狀。



S08 · implies操作前

\forall a\,b,\ a\le b\to a<b+1

操作後

(a,b)=(3,3):\ 3\le 3\to 3<4;\quad (a,b)=(5,2):\ 5\le 2\to 5<3

條件：無

規則：forall_elim · 依賴：S03

葉節點依據：forall_elim + numeric_evaluation

用兩個實例看清陳述的意思。a=b=3 時假設 3≤3 成立，結論 3<4 也成立。a=5、b=2 時假設 5≤2 不成立，陳述對這一對不要求結論 5<3（在古典讀法中這個蘊含空真）。假設限定了陳述對哪些數對宣稱結論。



S09 · theorem_application操作前

\forall a,b\in\mathbb{N},\ a\le b\Rightarrow a<b+1

操作後

\text{true in}\ \mathbb{N}\ \text{(informal proof)}

條件：無

規則：L_main · 依賴：S03

葉節點依據：order_basics + forall_intro + imp_intro

套用引理 L_main（在 S09.1、S09.2 證明）：在標準自然數中，陳述的數學內容成立。這是數學上的非正式證明，對應 S07 中 q 的構造計畫。



S10 · implies操作前

\text{informal proof of the content of}\ S

操作後

\mathsf{Parse},\ \mathsf{Elab},\ \mathsf{Kernel}:\ \text{not run};\ p:\ \text{not constructed}

條件：無

規則：mko_lean_formal_statement_def · 依賴：S06, S07, S09

葉節點依據：mko_lean_formal_statement_def + lean_stages + mko_proposition_def

整理狀態。S09 證明了陳述的數學內容在標準 ℕ 中為真，並給出 S07 中 q 的構造計畫；但它不是 Lean 證明項，也沒有任何東西經過 kernel check。因此狀態表為：解析未執行；elaboration 未執行；Prop 型別只有手工分析（S05，以 elaboration 成功為前提）；證明項未建立；kernel check 未執行。依 MKO，形式陳述與其已檢查證明項是分離狀態，本稿只推進了前者的概念分析。



S11 · implies操作前

s'=\texttt{∀ (a : Nat), a - 1 < a}

操作後

\Gamma\vdash S':\mathrm{Prop}\quad(\text{conditional on}\ \mathsf{Elab}(s'))

條件：\mathsf{Elab}(s')\ \text{succeeds (not run)}

規則：prop_formation · 依賴：G4, S05

葉節點依據：prop_formation + lean_core_notation

對 s′ 重做 S05 的型別分析：a−1 是 HSub Nat Nat Nat 的值，型別 Nat；LT.lt (a−1) a : Prop；對 a : Nat 全稱量化仍是 Prop。所以若 s′ 能 elaboration，它同樣表達一個形式陳述。



S12 · implies操作前

\forall a:\mathrm{Nat},\ a-1<a

操作後

a=0:\ 0-1=0,\ \neg(0<0)\ \Rightarrow\ \neg\forall a,\ a-1<a

條件：\text{truncated subtraction on Nat}

規則：quantifier_negation · 依賴：S11

葉節點依據：nat_trunc_sub + quantifier_negation + order_basics

在 Nat 的截斷減法下，a=0 給出 0−1=0（S12.1），而 0<0 不成立（S12.2）。存在反例，依量詞否定，S′ 的內容在標準讀法下為假。S′ 是 Prop（S11）但不是真命題：是命題不表示已證明為真（mko_proposition_def）。



S13 · implies操作前

s''=\texttt{∀ (a : Int), a - 1 < a}

操作後

\forall a\in\mathbb{Z},\ a-1<a\ \text{(true)};\quad S''\ne S'

條件：\text{ring subtraction on Int}

規則：order_basics · 依賴：G4, S12

葉節點依據：order_basics + nat_trunc_sub

在 Int 上減法是通常的環減法。對任意整數 a，−1<0，兩邊加 a 得 a−1<a，所以 S″ 的內容為真。s′ 與 s″ 只差一個型別名稱，但約束變數型別不同、減法不同，因此是不同的核心項，而且真假不同。型別與環境都是陳述身分的一部分（MKO 假設 a1）。



S14 · implies操作前

t_0=\texttt{a ≤ b → a < b + 1}

操作後

\text{meaning of}\ t_0\ \text{depends on}\ \Gamma\ \text{and elaborator options}

條件：無

規則：mko_lean_formal_statement_def · 依賴：S01, S03

葉節點依據：mko_lean_formal_statement_def + lean_stages

去掉約束後的文字 t0。若 local context 是 Γ′=(a b : Nat)，t0 會被讀成關於這兩個區域變數的陳述；在 E 的空 Γ 中，a、b 不是已宣告名稱，elaboration 可能失敗，也可能依 elaborator 選項（例如自動隱式約束）以不同方式處理，本稿不預測是哪一種。所以 receipt 必須記錄 Γ 與選項；同一段文字在不同 context 中不是同一個陳述。







## 局部子步與引理

S05.1 · implies操作前

\Gamma_1=(a:\mathrm{Nat},\ b:\mathrm{Nat})

操作後

\Gamma_1\vdash b+1:\mathrm{Nat},\ \Gamma_1\vdash a\le b:\mathrm{Prop},\ \Gamma_1\vdash a<b+1:\mathrm{Prop}

條件：無

規則：lean_core_notation · 依賴：S04

葉節點依據：lean_core_notation

在加入兩個約束變數後的 context Γ1 中：HAdd Nat Nat Nat 的輸出型別是 Nat，所以 b+1 : Nat；LE.le 與 LT.lt 的型別是 Nat → Nat → Prop，套用到兩個 Nat 就得到 Prop。



S05.2 · implies操作前

\Gamma_1\vdash a\le b:\mathrm{Prop},\ \Gamma_1\vdash a<b+1:\mathrm{Prop}

操作後

\Gamma_1\vdash (a\le b\to a<b+1):\mathrm{Prop}

條件：無

規則：prop_formation · 依賴：S05.1

葉節點依據：prop_formation

依規則 (i)：兩個 Prop 之間的蘊含仍是 Prop。



S05.3 · implies操作前

\Gamma_1\vdash (a\le b\to a<b+1):\mathrm{Prop}

操作後

\Gamma\vdash \forall a:\mathrm{Nat},\ \forall b:\mathrm{Nat},\ (a\le b\to a<b+1):\mathrm{Prop}

條件：\mathrm{Nat}:\mathrm{Type}=\mathrm{Sort}\ 1

規則：prop_formation · 依賴：S05.2

葉節點依據：prop_formation

依規則 (ii) 兩次：先在 context (a:Nat) 中約束 b，得到 ∀b:Nat, (a≤b → a<b+1) : Prop；再在空 context Γ 中約束 a。因為 Nat : Type，而 Prop 是非直謂的，對任何型別量化一個 Prop 仍得 Prop。三個子步合起來給出 S05 的結論。



S09.1 · implies操作前

0<1

操作後

b<b+1

條件：b\in\mathbb{N}

規則：order_basics · 依賴：order_basics

葉節點依據：order_basics

由 0<1，兩邊同加 b（次序對加法保持），得 b<b+1。把 ℕ 視為 ℝ 的子集，使用同一個次序。



S09.2 · implies操作前

a\le b,\ b<b+1

操作後

a<b+1

條件：a\le b

規則：case_analysis · 依賴：S09.1, order_basics

葉節點依據：case_analysis + order_basics + eq_replace + imp_intro + forall_intro

a≤b 表示 a<b 或 a=b。若 a<b，與 b<b+1 依傳遞得 a<b+1；若 a=b，把 b 換成 a 代入 b<b+1 直接得 a<b+1。兩種情況都得結論；a、b 是任意的，釋放假設並全稱推廣，L_main 得證。



S12.1 · implies操作前

0-1\ \text{in Nat}

操作後

0-1=0

條件：0\le 1

規則：nat_trunc_sub · 依賴：nat_trunc_sub

葉節點依據：nat_trunc_sub

因為 0≤1，截斷減法給出 0−1=0，而不是 −1；−1 不是自然數。



S12.2 · equivalent操作前

0-1<0

操作後

0<0,\ \text{which is false}

條件：無

規則：eq_replace · 依賴：S12.1, order_basics

葉節點依據：eq_replace + order_basics

以 0−1=0 代換，0−1<0 等價於 0<0；依三分律 0=0 時 0<0 不成立。







## 逐步反向審查


- S14 · premise_audit · S01, mko_lean_formal_statement_def, lean_stages — 此步只陳述依賴關係，不宣稱 t0 在任何環境中的實際 elaboration 結果。
- S13 · premise_audit · G4, nat_trunc_sub, order_basics — 需要 Int 減法的通常定義（引用）與次序對加法保持。N6 只在有限範圍核對，不取代全稱證明。
- S12.2 · inverse_equivalence · S12.1, eq_replace — 以相等的式子代換不改變真假，兩向都成立。
- S12.1 · premise_audit · nat_trunc_sub — 結論依賴 Nat 減法的定義；在 Int 中同一式子等於 −1（見 S13）。
- S12 · premise_audit · nat_trunc_sub, quantifier_negation, mko_proposition_def — 需要引用的截斷減法定義（citation_verified）。一個反例足以否定全稱陳述（N4、N5 可重算）。
- S11 · premise_audit · G4, prop_formation, lean_core_notation — 與 S05 一樣是以 elaboration 成功為前提的手工分析；結論只到「是 Prop」。
- S10 · premise_audit · S06, S07, S09, mko_lean_formal_statement_def, G2 — 此步的作用是阻止升級：數學上為真與非正式證明都不能推出 Γ⊢p:S 已被 kernel 接受。
- S09.2 · premise_audit · S09.1, order_basics, case_analysis, imp_intro, forall_intro — 兩種情況涵蓋 a≤b 的全部可能；不宣稱反向（a<b+1 ⇒ a≤b 在 ℕ 中其實也成立，但這裡沒用到也沒證明）。
- S09.1 · premise_audit · order_basics — 只用到 u<v ⇒ u+w<v+w。
- S09 · premise_audit · L_main — 結論是關於標準 ℕ 的數學事實，不是關於 Lean 的任何狀態；它不產生證明項，也不經 kernel check。N3 只在 0 到 6 的 49 個數對上做有限核對，不取代引理的證明。
- S08 · premise_audit · S03, forall_elim — 實例化只把全稱陳述用到特定值；兩個實例不能證明全稱陳述（N1、N2 只核對這兩個數值）。
- S07 · premise_audit · S04, curry_howard — 此步只描述證明項必須是什麼形狀；沒有造出任何 p，也沒有 kernel check。
- S06 · premise_audit · S05, mko_lean_formal_statement_def, G2 — 此步不宣稱前件已成立，所以不能把後件當作已確認。它也不宣稱 S 為真或已證明：是陳述與已證明是分離狀態。
- S05.3 · premise_audit · S05.2, prop_formation — 需要 Nat 是一個型別（Sort 1）以及規則 (ii)。結論是 S 屬於 Prop，與 S 是否可證無關。
- S05.2 · premise_audit · S05.1, prop_formation — 只需兩邊都是 Prop；不宣稱蘊含為真。
- S05.1 · premise_audit · lean_core_notation — 需要引用的 LE、LT、HAdd 型別簽名。這只說 a≤b 是命題，不說它為真。
- S05 · premise_audit · S04, prop_formation — 需要 S04 的條件式前提與引用的型別規則；若 elaboration 給出不同的項，這個分析要重做。
- S04 · premise_audit · S03, lean_core_notation, G2 — 此步是條件式：以 Elab(s) 成功為前提。若 E 中缺少任一 instance 或記號，elaboration 會失敗，S 根本不存在。
- S03 · premise_audit · G3, lean_core_notation — 閱讀依賴 E 中的記號與優先序；不同 imports 可能重新定義記號而得到不同結構（MKO 第二段）。不宣稱解析器接受 s。
- S02 · premise_audit · lean_stages, mko_lean_formal_statement_def — 階段劃分來自引用的 Lean 文件（citation_verified）。此步只定義狀態名稱，不宣稱任何狀態已達成。
- S01 · premise_audit · G1, G2, mko_lean_formal_statement_def — 此步只命名，不推出新事實。V 尚未釘選，這是待處理項，不影響後面以 E 為參數的條件式分析。





## 錯誤控制與反例

四種狀態不是同一件事MKO 指出的誤解是把成功解析、成功 elaboration、型別為 Prop 與已通過 kernel 的證明視為同一件事。S02 把它們分成五個狀態；s′ 說明即使前幾個狀態都達成（若 elaboration 成功），陳述仍可能為假，因此不可能有證明。本稿只有手工分析，任何狀態都沒有執行。

文字相同不等於陳述相同s′ 與 s″ 只差 Nat 與 Int，卻是不同的核心項，一假一真（S12、S13）；t0 在不同 local context 中意義不同（S14）。比對陳述時必須比較環境與核心項，不能只比字串。

非正式證明不是已檢查的證明項S09 的論證證明了數學內容，並提供證明項的構造計畫（S07），但它不是 Lean 項，也沒有經過 kernel。把它寫成「已由 Lean 證明」是錯誤的升級。


- s 看起來是合法的 Lean，所以它在任何環境中都能 elaboration → reject — elaboration 依賴版本、imports、記號、instance 與 local context（MKO 假設 a1）；本稿也沒有執行 elaboration。
- S 的型別是 Prop，所以 S 已被證明 → reject — S′ 同樣是 Prop，卻在 a=0 時為假：0−1=0 而 0<0 不成立。
- 本稿顯示 s 可以編譯，且定理已由 Lean 證明 → reject — G2：本稿沒有執行 Lean，沒有任何解析、elaboration 或 kernel receipt。
- s′ 與 s″ 只差型別名稱，所以是同一個陳述 → reject — 型別與減法不同，s′ 在 a=0 為假而 s″ 對所有整數為真。





## 結論與限制

s 讀作「對所有自然數 a、b，若 a≤b 則 a<b+1」：兩個 Nat 約束變數、一個假設 a≤b、一個結論 a<b+1。若在 E 中 elaboration 成功，核心項 S 的型別依型別規則為 Prop，於是 s 表達一個形式陳述；其證明項必須是接收 a、b 與 h:a≤b 並回傳 a<b+1 證明的函數。其數學內容在標準 ℕ 中為真（非正式證明）。本稿沒有執行 Lean：解析、elaboration、證明項與 kernel check 的狀態都是「未執行」。s′ 是 Prop 但在 a=0 時為假，s″ 為真，顯示型別與環境屬於陳述身分。


- 使用者恢復 Lean 工作後，應釘選 toolchain 版本與 import closure，並為 s、s′、s″ 記錄解析與 elaboration receipt；若要證明 s，需建立證明項並取得 kernel receipt（MKO formal next）。
- S04 顯示的核心項省略了隱式與 instance 參數，確切形式（含 instance 名稱）只能由實際 elaboration 確定。所引用的記號、型別規則與截斷減法已對照 Lean 官方文件和列出的核心來源；未執行 Lean，也未取得 elaboration 或 kernel receipt。





## 驗證及來源綁定

6 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 5cb0d5f28f6aea7530d0c886c4ff344564b3ecefcd4d14d3748e25c6afef4cd2
- original source SHA-256: 5cb0d5f28f6aea7530d0c886c4ff344564b3ecefcd4d14d3748e25c6afef4cd2
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-lean-formal-statement-01.json)