# 證明項：逐部分解讀 λh. ⟨snd h, fst h⟩ 為何是 P∧Q→Q∧P 的證明項 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-lean-proof-term/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-lean-proof-term-01 · production-20261019-adopted-96 ## 目標與範圍 在一個明示的合成小型命題型別系統 ST 中（對應 MKO 假設 a2），取相異命題原子 P、Q：逐部分說明項 t=λh:P∧Q. ⟨snd h, fst h⟩ 的每一部分建立了什麼、具有什麼型別，推導判斷 ⊢ t : P∧Q→Q∧P，並說明 t 的型別為什麼與命題 S=P∧Q→Q∧P 相符；再證明外觀相近的 t′=λh:P∧Q. ⟨fst h, snd h⟩ 不是 S 的證明項。最後區分「ST 中的型別推導」「Lean kernel 接受」與「已保存的 proof-term receipt」三者。 型別推導只在合成系統 ST 中進行；ST 的型別相等就是語法相同，沒有 Lean 的定義相等（conversion）、universe、implicit 參數或 elaboration。本稿不執行 Lean，不宣稱任何項已被 Lean 編譯、elaborate 或經 kernel 檢查，也不產生 Lean formal Evidence 或 receipt；文中的 Lean 4 表面寫法只是閱讀對照。不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - def_unfold - and_intro_elim - imp_intro - contradiction - G1 — 環境 E_ST 固定：P、Q 是兩個相異的命題原子，各自已作為命題給出（MKO 假設 a1）；型別由原子經 ∧ 與 → 組成。項、context 與規則表在全稿固定不變。 - G2 — ST 的規則表只有六條。Var：若 x:A 列在 Γ 中，則 Γ⊢x:A。∧I：由 Γ⊢a:A 與 Γ⊢b:B 得 Γ⊢⟨a,b⟩:A∧B。∧E1：由 Γ⊢p:A∧B 得 Γ⊢fst p:A。∧E2：由 Γ⊢p:A∧B 得 Γ⊢snd p:B。→I：由 Γ,x:A⊢b:B 得 Γ⊢λx:A.b : A→B。→E：由 Γ⊢f:A→B 與 Γ⊢a:A 得 Γ⊢f a:B。context 中每個變數至多出現一次；兩個型別相等當且僅當語法相同。 - G3 — 目標命題 S=P∧Q→Q∧P；待解讀的項 t=λh:P∧Q. ⟨snd h, fst h⟩；對照項 t′=λh:P∧Q. ⟨fst h, snd h⟩。 - G4 — 本稿沒有執行 Lean（MKO 假設 a2）：沒有 kernel 判斷，沒有保存的 term，也沒有 receipt。 - \Gamma_0,\ \Gamma_1 — 空 context；Γ0 加上假設 h:P∧Q - \Gamma\vdash u:A — 判斷：在 context Γ 中項 u 具有型別 A - \langle a,b\rangle — 配對建構子（∧ 引入） - \mathrm{fst}\,p,\ \mathrm{snd}\,p — 第一、第二投影（∧ 消去） - \lambda h{:}A.\,b — 以假設 h:A 做的函數抽象（→ 引入） - S — 目標命題 P∧Q→Q∧P - T(u) — 項 u 在給定 context 中推得的型別 ## 規則與來源 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - imp_intro · prerequisite — →引入（釋放假設）：若在暫時假設 P 的作用域中推出 Q，則得到 P⇒Q；此後 P 不再可當作已知使用。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。 - eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。 - modus_ponens · prerequisite — 肯定前件：由 P 與 P⇒Q 得 Q。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - mko_proof_term · cited — 在固定 Lean 版本、imports、環境 E 與 local context Γ 中，若核心項 t 具有命題 P 的型別，且 kernel 接受 Γ⊢t:P，則 t 是 P 的證明項。tactic log 只是建構過程，不等於已保存且可重播的 proof-term receipt。 · mko-lean-proof-term - mko_receipt · cited — tactic 成功且無 goals 通常產生候選 proof term；只有保存該 term 並經指定 kernel／環境檢查，才形成 receipt。kernel 接受只證形式 judgment；statement 是否忠實、imports 是否含不當公理是另外的義務。 · mko-lean-proof-term - st_var · prerequisite — ST 的 Var 規則：若 x:A 列在 Γ 中，則 Γ⊢x:A。 - st_and_intro · prerequisite — ST 的 ∧I 規則：由 Γ⊢a:A 與 Γ⊢b:B 得 Γ⊢⟨a,b⟩:A∧B；第一分量的型別成為左合取項。 - st_and_elim · prerequisite — ST 的 ∧E1、∧E2 規則：由 Γ⊢p:A∧B 得 Γ⊢fst p:A 與 Γ⊢snd p:B。 - st_imp_intro · prerequisite — ST 的 →I 規則：由 Γ,x:A⊢b:B 得 Γ⊢λx:A.b : A→B；結論的 context 中不再有 x（假設被釋放）。 - st_type_eq · prerequisite — ST 的型別相等就是語法相同：A∧B≡C∧D ⇔ A≡C 且 B≡D；A→B≡C→D ⇔ A≡C 且 B≡D；相異原子不相等。 - L_inversion · lemma — ST 的反演：每種外層項形式恰好是一條規則結論的主詞。所以若 Γ⊢u:A 可推導，則推導的最後一條規則就是 u 外層形式所對應的那條，其前提都可推導，且 A 具有該規則規定的形狀。 - L_tprime_untyped · lemma — 在 ST 中，判斷 Γ0⊢t′:P∧Q→Q∧P 不可推導，其中 t′=λh:P∧Q. ⟨fst h, snd h⟩。 ## 逐步主鏈 S01 · definition操作前 \text{proof term: fixed version, imports, environment }E,\ \Gamma,\ \text{kernel} 操作後 \text{ST: atoms }P\neq Q,\ \Gamma_0=\varnothing,\ S=P\land Q\to Q\land P,\ \text{six rules} 條件：無 規則：mko_proof_term · 依賴：G1, G2, G3, G4 葉節點依據：mko_proof_term + def_intro MKO 指出「證明項」只有在固定版本、imports、環境與 local context 之後才有意義。本稿固定一個教學用的對應物：環境 E_ST 只含原子 P、Q，起始 context Γ0 為空，目標命題 S=P∧Q→Q∧P，而「檢查器」的角色由 G2 的六條規則擔任：一個判斷只有在能用這六條規則逐條推出時才算成立。之後所有型別結論都是 ST 中的結論；關於 Lean 的陳述只在 S10 另外處理。 S02 · definition操作前 t 操作後 t=\lambda h{:}P\land Q.\,\langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle 條件：無 規則：def_intro · 依賴：S01, G3 葉節點依據：def_intro + def_unfold 為項取名並逐部分預讀它要建立的東西：λh:P∧Q 引入一個名為 h、型別為 P∧Q 的假設，讀作「假設有 P∧Q 的證明 h」；fst h 與 snd h 從 h 取出 P 與 Q 的證明；⟨·,·⟩ 把兩個證明裝成一個合取的證明，分量的先後決定合取項的先後。依命題即型別，蘊涵的證明是一個把前提的證明變成結論的證明的函數。Lean 4 中對應的表面寫法是 `fun h : P ∧ Q => And.intro h.right h.left`（或 `fun h => ⟨h.2, h.1⟩`），這裡只作閱讀對照。 S03 · implies操作前 \Gamma_1=\Gamma_0,\ h{:}P\land Q 操作後 \Gamma_1\vdash h:P\land Q 條件：h{:}P\land Q\in\Gamma_1 規則：st_var · 依賴：S02, G2 葉節點依據：st_var λ 的綁定說明本體要在哪個 context 中檢查：Γ1 是 Γ0 加上 h:P∧Q。依 Var 規則，h:P∧Q 列在 Γ1 中，所以 Γ1⊢h:P∧Q。這一部分建立的是：在本體內部，h 可以當作 P∧Q 的證明使用。 S04 · implies操作前 \Gamma_1\vdash h:P\land Q 操作後 \Gamma_1\vdash \mathrm{snd}\,h:Q 條件：A=P,\ B=Q 規則：st_and_elim · 依賴：S03, G2 葉節點依據：st_and_elim 對 S03 使用 ∧E2，取 A=P、B=Q：snd h 取出第二分量，型別為 Q。這一部分建立了「由假設得到 Q 的證明」。snd h 的型別是從 h 的型別讀出來的，不是自行指定的。 S05 · implies操作前 \Gamma_1\vdash h:P\land Q 操作後 \Gamma_1\vdash \mathrm{fst}\,h:P 條件：A=P,\ B=Q 規則：st_and_elim · 依賴：S03, G2 葉節點依據：st_and_elim 對 S03 使用 ∧E1：fst h 取出第一分量，型別為 P。現在 Γ1 中同時有 P 的證明與 Q 的證明，而且兩者都只依賴假設 h。 S06 · implies操作前 \Gamma_1\vdash \mathrm{snd}\,h:Q,\ \ \Gamma_1\vdash \mathrm{fst}\,h:P 操作後 \Gamma_1\vdash \langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:Q\land P 條件：a=\mathrm{snd}\,h,\ A=Q,\ b=\mathrm{fst}\,h,\ B=P 規則：st_and_intro · 依賴：S04, S05 葉節點依據：st_and_intro 使用 ∧I，第一分量 a=snd h（型別 A=Q），第二分量 b=fst h（型別 B=P），得到 A∧B=Q∧P。合取項的先後由分量的先後決定：第一分量的型別成為左合取項。這一部分建立了「由 P∧Q 的假設得到 Q∧P 的證明」。 S07 · implies操作前 \Gamma_0,\ h{:}P\land Q\vdash \langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:Q\land P 操作後 \Gamma_0\vdash \lambda h{:}P\land Q.\,\langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:P\land Q\to Q\land P 條件：x=h,\ A=P\land Q,\ B=Q\land P 規則：st_imp_intro · 依賴：S06, S03 葉節點依據：st_imp_intro + imp_intro 使用 →I，x=h、A=P∧Q、B=Q∧P：釋放假設 h，結論位於 Γ0，其中已沒有 h。綁定上的註記 P∧Q 成為蘊涵的前件，本體的型別 Q∧P 成為後件。這正是 →引入（imp_intro）在命題即型別下的讀法：在假設 P∧Q 的作用域中得到 Q∧P，就得到 P∧Q→Q∧P。 S08 · implies操作前 T(t)=P\land Q\to Q\land P,\ \ S=P\land Q\to Q\land P 操作後 T(t)\equiv S 條件：無 規則：st_type_eq · 依賴：S07, G3 葉節點依據：st_type_eq + eq_refl_symm_trans MKO 的公式 T(t)=P 要求推得的型別與命題相同（本稿把命題記為 S，以免與原子 P 混淆）。逐符號比較：前件 P∧Q 對 P∧Q，後件 Q∧P 對 Q∧P，完全相同，所以在 ST 中 T(t)≡S。Lean 的型別比對是到定義相等為止，範圍較寬；ST 只用語法相同，所以這裡沒有使用任何 conversion。 S09 · implies操作前 \Gamma_0\vdash t:T(t),\ \ T(t)\equiv S 操作後 t\ \text{is a proof term for }S\ \text{in ST} 條件：無 規則：mko_proof_term · 依賴：S07, S08, mko_proof_term 葉節點依據：mko_proof_term + modus_ponens + eq_replace MKO 的定義要求兩件事：項的型別就是該命題，而且固定環境的檢查器接受這個判斷。在 ST 中檢查器就是規則表：S03 到 S07 每一步都是 G2 的一條規則，構成 Γ0⊢t:T(t) 的完整推導；S08 把 T(t) 與 S 等同，所以 Γ0⊢t:S 可推導，這是「kernel 接受 Γ⊢t:P」在 ST 中的對應。因此 t 是 S 在 ST 中的證明項；此步宣稱的就只有這些。 S10 · implies操作前 t\ \text{proof term in ST};\ \text{Lean not run} 操作後 \text{Lean counterpart: candidate term, no kernel verdict, no receipt} 條件：無 規則：mko_receipt · 依賴：S09, G4, mko_receipt 葉節點依據：mko_receipt + modus_ponens 依 MKO，只有保存 term 並在指定 kernel／環境中檢查，才形成 receipt。G4 說明本稿沒有執行 Lean，沒有保存也沒有檢查任何 term。所以 Lean 4 對應寫法 `fun h : P ∧ Q => And.intro h.right h.left` 的狀態只是候選 proof term：不宣稱 kernel 接受，也沒有 receipt。ST 的推導不能代替 kernel 判斷，因為兩者是不同的系統（Lean 另有 universe、定義相等與 elaborator）。即使日後 kernel 接受，也只證形式 judgment；命題是否忠實表達原意、imports 是否含不當公理仍需另外審查。 S11 · implies操作前 \text{rule table of ST} 操作後 \text{each outer term form is concluded by exactly one rule} 條件：無 規則：case_analysis · 依賴：G2 葉節點依據：case_analysis + def_unfold 逐條檢查六條規則結論中主詞的外層形式：Var 是變數；∧I 是配對 ⟨a,b⟩；∧E1 是 fst p；∧E2 是 snd p；→I 是 λx:A.b；→E 是應用 f a。六條規則對應六種互不相同的形式，而每個項恰有一種外層形式。Γ⊢u:A 的推導必以某條結論為 Γ⊢u:A 的規則結束，所以最後一條規則就是 u 的外層形式所對應的唯一規則，其前提必在其上方已被推出，A 也必具該規則規定的形狀。這證明了引理 L_inversion。 S12 · implies操作前 t'=\lambda h{:}P\land Q.\,\langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle 操作後 \Gamma_0\nvdash t':P\land Q\to Q\land P 條件：無 規則：L_tprime_untyped · 依賴：G3, L_tprime_untyped 葉節點依據：L_inversion + st_type_eq + contradiction 依引理 L_tprime_untyped（在 S12.1 到 S12.4 證明），t′ 在 ST 中不能具有型別 S。所以 t′ 不是 S 的證明項，即使它用到同一個假設與同樣兩個投影。 S13 · implies操作前 \Gamma_1\vdash \mathrm{fst}\,h:P,\ \ \Gamma_1\vdash \mathrm{snd}\,h:Q 操作後 \Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:P\land Q 條件：a=\mathrm{fst}\,h,\ A=P,\ b=\mathrm{snd}\,h,\ B=Q 規則：st_and_intro · 依賴：S04, S05 葉節點依據：st_and_intro 看看 t′ 實際證明了什麼：分量次序為 fst h、snd h，∧I 給出 P∧Q，而不是 Q∧P。差別只在分量次序，但型別因此不同。 S14 · implies操作前 \Gamma_0,\ h{:}P\land Q\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:P\land Q 操作後 \Gamma_0\vdash t':P\land Q\to P\land Q 條件：x=h,\ A=P\land Q,\ B=P\land Q 規則：st_imp_intro · 依賴：S13 葉節點依據：st_imp_intro + imp_intro 對 S13 使用 →I 並釋放 h：t′ 是 P∧Q→P∧Q 的證明項，這是另一個命題。所以「是否為 S 的證明項」取決於確切的型別，而不是取決於用到哪些假設或投影。 S15 · implies操作前 \Gamma_0\vdash t:S,\ \Gamma_0\nvdash t':S,\ \text{Lean not run} 操作後 t\ \text{proves }S\ \text{in ST};\ t'\ \text{does not};\ \text{no Lean receipt} 條件：無 規則：and_intro_elim · 依賴：S09, S10, S12, S14 葉節點依據：and_intro_elim 合併三個結論：t 是 S 在 ST 中的證明項（S09）；t′ 不是（S12），它證明的是 P∧Q→P∧Q（S14）；Lean 方面只有候選項，沒有 kernel 判斷與 receipt（S10）。 ## 局部子步與引理 S12.1 · implies操作前 \Gamma_0\vdash t':P\land Q\to Q\land P\ \ (\text{assumed}) 操作後 \Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:Q\land P 條件：無 規則：L_inversion · 依賴：G3, L_inversion 葉節點依據：L_inversion + st_type_eq 為了反證，假設 Γ0⊢t′:S 有推導。t′ 的外層形式是 λ，依 L_inversion 最後一條規則必為 →I，其結論型別 A→B 中 A 是綁定註記 P∧Q；由 A→B≡P∧Q→Q∧P 得 B≡Q∧P。所以前提 Γ0,h:P∧Q⊢⟨fst h, snd h⟩:Q∧P 可推導，也就是 Γ1⊢⟨fst h, snd h⟩:Q∧P。 S12.2 · implies操作前 \Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:Q\land P 操作後 \Gamma_1\vdash \mathrm{fst}\,h:Q 條件：無 規則：L_inversion · 依賴：S12.1, L_inversion 葉節點依據：L_inversion + st_type_eq 配對只能由 ∧I 推出，其結論型別 A∧B 中 A 是第一分量的型別。由 A∧B≡Q∧P 得 A≡Q，所以前提 Γ1⊢fst h:Q 必須可推導。 S12.3 · implies操作前 \Gamma_1\vdash \mathrm{fst}\,h:Q 操作後 \Gamma_1\vdash h:Q\land B\ \text{for some type }B 條件：無 規則：L_inversion · 依賴：S12.2, L_inversion 葉節點依據：L_inversion fst 的形式只能由 ∧E1 推出，其前提是 Γ1⊢h:A∧B 且結論型別為 A。這裡 A≡Q，所以存在某個型別 B 使 Γ1⊢h:Q∧B 可推導。 S12.4 · implies操作前 \Gamma_1\vdash h:Q\land B 操作後 Q\land B\equiv P\land Q\Rightarrow Q\equiv P\ \ (\text{contradiction}) 條件：P\not\equiv Q 規則：contradiction · 依賴：S12.3, G1, G2, L_inversion 葉節點依據：st_var + st_type_eq + contradiction 變數只能由 Var 推出，所以 h:Q∧B 必須就是 Γ1 中 h 的條目；Γ1 只列 h 一次，型別為 P∧Q，故 Q∧B≡P∧Q。依 st_type_eq 逐分量比較得 Q≡P，與 G1 中 P、Q 為相異原子矛盾。所以 S12.1 的假設不成立，Γ0⊢t′:S 不可推導。S12.1 到 S12.4 合起來證得引理 L_tprime_untyped。 ## 逐步反向審查 - S15 · sufficient_goal_reduction · S09, S10, S12, S14, and_intro_elim — 目標 G：本稿目標中的三項判定。足夠條件 H：S09、S12、S10 三個已證結論（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。 - S14 · premise_audit · S13, st_imp_intro — 與 S07 相同的 →I 用法；結合 S12，t′ 的型別是 P∧Q→P∧Q 而不能是 S。 - S13 · premise_audit · S04, S05, st_and_intro — 重用 S04、S05 的兩個判斷，只是以另一種次序配對。 - S12.4 · premise_audit · S12.3, G1, st_var, st_type_eq, contradiction — 矛盾需要兩件事：context 中每個變數只出現一次（G2），以及 P、Q 相異（G1）。若 P 與 Q 是同一個原子，t′ 就會有型別 S，所以這個前提不可省略。 - S12.3 · premise_audit · S12.2, L_inversion — B 是 ∧E1 前提中出現的某個型別，我們不需要知道它是什麼；仍在反證假設之下。 - S12.2 · premise_audit · S12.1, L_inversion, st_type_eq — 只用反演與合取型別的逐分量比較；仍在反證假設之下。 - S12.1 · premise_audit · L_inversion, st_type_eq — 用到 λ 項只能由 →I 推出，以及 A→B≡P∧Q→Q∧P 迫使 B≡Q∧P。這是反證法中的暫時假設，在 S12.4 釋放。 - S12 · premise_audit · L_tprime_untyped — 依賴該引理；引理的證明只用到反演與 P、Q 相異。 - S11 · premise_audit · G2, case_analysis — 分情況是完整的，因為 G2 列出了 ST 的全部規則（只有六條）。若系統另有 conversion 規則或第二條配對規則，反演需要更多情況；這也是本論證不能原封不動搬到 Lean 的原因之一。 - S10 · premise_audit · G4, S09, mko_receipt — 只需要「沒有發生 kernel 檢查」這一事實。方向是「未檢查 ⇒ 無 receipt」；此步也不宣稱 Lean 會拒絕這個項，它對 Lean 的判斷不作任何宣稱。 - S09 · premise_audit · S07, S08, mko_proof_term — 需要一個完整的推導（每一步一條規則）與型別相符。結論只屬於 ST，不轉移到 Lean（見 S10）。 - S08 · premise_audit · S07, G3, st_type_eq — 需要 S07 推得的型別與 G3 的命題；比較的是型別而不是真值。Q∧P 與 P∧Q 邏輯等價，卻不是同一個型別（見錯誤控制）。 - S07 · premise_audit · S06, st_imp_intro, imp_intro — →I 需要本體的判斷位於「Γ0 恰好加上 h:P∧Q」的 context，S06 提供的正是 Γ1。釋放之後 h 不可再當作已知使用。 - S06 · premise_audit · S04, S05, st_and_intro — ∧I 需要兩個前提位於同一個 context，S04、S05 都在 Γ1。型別 Q∧P 是由分量次序強制的；若把分量對調，得到的是 P∧Q（見 S13）。 - S05 · premise_audit · S03, st_and_elim — 與 S04 相同，只需要 h 的合取型別；結果與 S04 位於同一個 context Γ1，這是 S06 的前提。 - S04 · premise_audit · S03, st_and_elim — ∧E2 需要 h 具有合取型別，S03 提供 P∧Q。不宣稱反向：由 Q 的證明不能得到 P∧Q 的證明。 - S03 · premise_audit · G2, st_var — Var 只需要 h:P∧Q 列在 Γ1 中。不宣稱反向：在 Γ0 中 h 沒有宣告，Γ0⊢h:P∧Q 不成立，所以本體必須在 Γ1 中檢查。 - S02 · premise_audit · G3, def_intro — 此步只取名；對各部分的解讀是一個計畫，必須由 S03 到 S07 逐條規則證成。這裡尚未宣稱 t 有任何型別。 - S01 · premise_audit · G1, G2, G4, mko_proof_term — 此步只固定設定，不推出新事實。以 ST 規則表代替 kernel 是 G2、G4 明示的教學選擇，不是關於 Lean 的證據。 ## 錯誤控制與反例 tactic 紀錄、零 goals 與自報都不是 receipt例如 tactic 稿 `intro h; exact ⟨h.2, h.1⟩` 顯示沒有剩餘 goals，只說明建構過程看起來完成了。依 MKO，receipt 需要保存下來的 term，以及在指定 toolchain、imports 與環境中由 kernel 檢查的結果。成功編譯的訊息或模型自報同理，都不能代替保存且可重播的 kernel 判斷。本稿 S10 因此只給出 candidate 狀態。 型別要完全相符，不是用到 P 和 Q 就好t′ 用到同一個假設與兩個投影，型別卻是 P∧Q→P∧Q；S12 以反演證明它不能具有型別 S。另外，Q∧P 與 P∧Q 在每個真值賦值下真假相同（N2），但它們不是同一個型別；兩者的邏輯等價需要兩個方向的證明；t 只建立 P∧Q→Q∧P，反方向需另給相應的交換證明項。即使建立了等價，也不能取代此語法系統的型別比對。 ST 推導不是 Lean kernel 檢查ST 只有六條規則與語法相等；Lean 另有 universe、定義相等、elaboration 與 implicit 參數。本稿的推導說明證明項的結構，不證明任何 Lean 檔案可以編譯。即使 kernel 接受，也只證形式 judgment；命題是否忠實、imports 是否含不當公理仍需另外審查（MKO 第三段）。 - tactic `intro h; exact ⟨h.2, h.1⟩` 顯示沒有 goals，所以已經有 kernel 接受的 proof-term receipt → reject — 零 goals 是建構過程的狀態；receipt 需要保存 term 並在指定環境經 kernel 檢查，本稿兩者都沒有（G4、S10）。 - t′=λh:P∧Q. ⟨fst h, snd h⟩ 也是 P∧Q→Q∧P 的證明項，因為它用了同一個假設與兩個投影 → reject — 依反演，這要求 Q≡P，與 P、Q 相異矛盾（S12.4）；t′ 的型別是 P∧Q→P∧Q（S14）。 - 既然 ST 中 ⊢t:S 可推導，Lean 的 kernel 已經接受 `fun h : P ∧ Q => And.intro h.right h.left` → reject — ST 是合成的教學系統，本稿沒有執行 Lean；一個系統中的推導不代表另一個檢查器的判斷。 - 若 kernel 接受 Γ⊢t:S，則 S 必然忠實表達原始中文命題，imports 也沒有不當公理 → reject — MKO 指出 kernel 接受只證形式 judgment；忠實性與公理清單是另外的語義與信任義務。 ## 結論與限制 在合成系統 ST 中，t=λh:P∧Q. ⟨snd h, fst h⟩ 的各部分依次建立：h 是 P∧Q 的假設，snd h 與 fst h 分別是 Q、P 的證明，配對給出 Q∧P，釋放 h 得到 P∧Q→Q∧P；此型別與 S 逐符號相同，所以 t 是 S 在 ST 中的證明項。t′=λh:P∧Q. ⟨fst h, snd h⟩ 的型別是 P∧Q→P∧Q，依反演它不能具有型別 S。本稿沒有執行 Lean：Lean 4 對應項只是候選，沒有 kernel 判斷，也沒有 receipt。 - N1 到 N3 是對四個布林賦值的真值表核對，這四點就是全部賦值；它們只涉及古典真值，不涉及型別，本稿的型別論證不依賴它們。 - →E 規則在本稿的推導中沒有用到，列入規則表是為了讓 S11 的反演分情況完整。 - Lean 方面的 receipt（固定 toolchain、imports、公理清單與保存的 term）留待 OCME 主負責人恢復 Lean 工作後處理。 ## 驗證及來源綁定 3 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: e911f6af08dca1ddcd82398376624ff01b2bc98988791c2202ae47e5512c751c - original source SHA-256: a17503af594b30f3d269250d35760be89786b5b022f96578e7977e5d3be7c2da - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-lean-proof-term-01.json)