證明項：逐部分解讀 λh. ⟨snd h, fst h⟩ 為何是 P∧Q→Q∧P 的證明項

目標與範圍

在一個明示的合成小型命題型別系統 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⟩。

逐步主鏈

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

t

t=\lambda h{:}P\land Q.\,\langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle

\Gamma_1=\Gamma_0,\ h{:}P\land Q

\Gamma_1\vdash h:P\land Q

\Gamma_1\vdash h:P\land Q

\Gamma_1\vdash \mathrm{snd}\,h:Q

\Gamma_1\vdash h:P\land Q

\Gamma_1\vdash \mathrm{fst}\,h:P

\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

\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

T(t)=P\land Q\to Q\land P,\ \ S=P\land Q\to Q\land P

T(t)\equiv S

\Gamma_0\vdash t:T(t),\ \ T(t)\equiv S

t\ \text{is a proof term for }S\ \text{in ST}

t\ \text{proof term in ST};\ \text{Lean not run}

\text{Lean counterpart: candidate term, no kernel verdict, no receipt}

\text{rule table of ST}

\text{each outer term form is concluded by exactly one rule}

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

\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

\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

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

局部子步與引理

\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

\Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:Q\land P

\Gamma_1\vdash \mathrm{fst}\,h:Q

\Gamma_1\vdash \mathrm{fst}\,h:Q

\Gamma_1\vdash h:Q\land B\ \text{for some type }B

\Gamma_1\vdash h:Q\land B

Q\land B\equiv P\land Q\Rightarrow Q\equiv P\ \ (\text{contradiction})

逐步反向審查

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