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

目標與範圍

以源碼字串 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。

逐步主鏈

s,\ E

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

s

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

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)

\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))

S

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

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

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

\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

\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 a,b\in\mathbb{N},\ a\le b\Rightarrow a<b+1

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

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

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

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

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

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

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

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

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

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

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

局部子步與引理

\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}

\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}

\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}

0<1

b<b+1

a\le b,\ b<b+1

a<b+1

0-1\ \text{in Nat}

0-1=0

0-1<0

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

逐步反向審查

• 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、反控制與修訂記錄）