# 子集合：以任意元素證明包含，並以反例否定包含 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-subset/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-subset-01 · production-20261019-adopted-96 ## 目標與範圍 在論域 ℤ 中，令 A 為 6 的倍數之集、B 為偶數之集、C 為 4 的倍數之集。證明 A⊆B，且這個包含是嚴格的（A≠B）；證明 A⊄C，雖然 A 與 C 有共同元素 12；說明 B⊆B 成立（⊆ 允許相等）；並證明 {6}⊆A ⇔ 6∈A，同時分辨兩個語句的型別角色。 只處理同一論域 ℤ 中的集合（MKO 假設 a1），示範子集合定義的展開、證明與否定。整數的乘法封閉性與離散性作為前置知識使用，不從整數公理推出。不綁定 Lean 的 Set.Subset 定義；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - set_builder - subset_def - int_closure - int_discrete - order_basics - G1 — 論域是整數集合 ℤ；本稿所有集合都是 ℤ 的子集合，因此任兩個都在同一論域中（MKO 假設 a1）。 - G2 — A={n∈ℤ ∣ 存在 k∈ℤ 使 n=6k}，B={n∈ℤ ∣ 存在 m∈ℤ 使 n=2m}，C={n∈ℤ ∣ 存在 j∈ℤ 使 n=4j}。 - \mathbb{Z} — 整數集合，本稿的論域 - A,B,C — 6 的倍數、偶數、4 的倍數之集 - A\subseteq B — A 是 B 的子集合（非嚴格包含） - A\subsetneq B — A 是 B 的嚴格子集合 - x\in A — 元素 x 屬於集合 A - \{a\} — 只含 a 的單元素集合 ## 規則與來源 - set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。 - subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。 - order_basics · prerequisite — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - imp_intro · prerequisite — →引入（釋放假設）：若在暫時假設 P 的作用域中推出 Q，則得到 P⇒Q；此後 P 不再可當作已知使用。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。 - set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。 - mko_subset_def · cited — 給定同一論域中的集合 A、B，A⊆B 當且僅當對每個對象 x，若 x∈A，則 x∈B。 · mko-subset - int_closure · prerequisite — 整數對加法與乘法封閉：若 a、b∈ℤ，則 a+b∈ℤ 且 ab∈ℤ。 - int_discrete · prerequisite — 整數的離散性：對整數 k 與整數 c，必有 k≤c 或 k≥c+1；c 與 c+1 之間沒有整數。 - proper_subset_def · prerequisite — 嚴格子集合：A⊊B 當且僅當 A⊆B 且 A≠B。 - neg_imp · prerequisite — 蘊涵的否定：¬(P⇒Q) 等價於 P∧¬Q。 - singleton_def · prerequisite — 單元素集合：x∈{a} 當且僅當 x=a。 - L_6k_ne_2 · lemma — 對每個整數 k，6k≠2。 - L_4j_ne_6 · lemma — 對每個整數 j，4j≠6。 - L_singleton_subset · lemma — 對任何集合 S 與同一論域中的對象 a：{a}⊆S ⇔ a∈S。 ## 逐步主鏈 S01 · definition操作前 \text{multiples of }6,\ \text{even integers},\ \text{multiples of }4\ \text{in }\mathbb{Z} 操作後 A=\{n\in\mathbb{Z}\mid\exists k\in\mathbb{Z},\ n=6k\},\ B=\{n\in\mathbb{Z}\mid\exists m\in\mathbb{Z},\ n=2m\},\ C=\{n\in\mathbb{Z}\mid\exists j\in\mathbb{Z},\ n=4j\} 條件：無 規則：def_intro · 依賴：G1, G2 葉節點依據：def_intro + set_builder 以集合建構式為三個集合取名。三者都由 ℤ 中的元素構成，所以它們在同一論域 ℤ 中，滿足 MKO 假設 a1；之後比較它們的包含關係才有意義。依 set_builder，n∈A 恰好表示 n∈ℤ 且有某個整數 k 使 n=6k；B、C 同理。 S02 · equivalent操作前 A\subseteq B 操作後 \forall x\ (x\in A\Rightarrow x\in B) 條件：A,B\subseteq\mathbb{Z} 規則：mko_subset_def · 依賴：S01, mko_subset_def 葉節點依據：mko_subset_def + subset_def + def_unfold 依 MKO 的定義展開目標：A⊆B 當且僅當對每個對象 x，x∈A 蘊涵 x∈B。對 ℤ 以外的對象，x∈A 為假，蘊涵自動成立，所以實際上只需對 x∈ℤ 檢查。這一步把一個關於兩個集合的語句，換成一個關於所有元素的全稱語句；要證明它，必須處理任意的 x，而不是挑選出來的幾個元素。 S03 · equivalent操作前 x\in A\ \ (x\in\mathbb{Z}\ \text{arbitrary}) 操作後 \exists k\in\mathbb{Z},\ x=6k 條件：x\in\mathbb{Z} 規則：set_builder · 依賴：S01, S02 葉節點依據：set_builder + def_unfold 取一個任意的 x∈ℤ，並暫時假設 x∈A（這個假設在 S07 釋放）。依 A 的集合建構式，x∈A 等價於「有某個整數 k 使 x=6k」。除了 x∈ℤ 與這個暫時假設之外，對 x 不加任何條件。 S04 · implies操作前 \exists k\in\mathbb{Z},\ x=6k 操作後 x=6k_0,\ k_0\in\mathbb{Z} 條件：無 規則：exists_elim · 依賴：S03 葉節點依據：exists_elim 依 ∃消去，給滿足條件的某個整數取新名字 k₀，得 x=6k₀。k₀ 只是那個整數的名字，最後的結論 x∈B 不會提到 k₀，所以這樣做是允許的。 S05 · equivalent操作前 x=6k_0 操作後 x=2(3k_0) 條件：無 規則：eq_replace · 依賴：S04 葉節點依據：numeric_evaluation + mul_assoc + eq_replace 把 6 寫成 2·3，再用乘法結合律：6k₀=(2·3)k₀=2(3k₀)。兩邊是同一個整數，所以等式的真假不變。這是本證明唯一的計算，而它對每個 k₀ 都成立（N1 以多項式恆等式核對）。 S06 · implies操作前 x=2(3k_0),\ k_0\in\mathbb{Z} 操作後 x\in B 條件：3k_0\in\mathbb{Z} 規則：exists_intro · 依賴：S04, S05, int_closure 葉節點依據：int_closure + exists_intro + set_builder 3 與 k₀ 都是整數，依整數的乘法封閉性 3k₀∈ℤ。於是 m=3k₀ 是一個使 x=2m 的整數；依 ∃引入與 B 的集合建構式，x∈B。 S07 · implies操作前 x\in A\ \text{assumed}\ \vdash\ x\in B,\quad x\in\mathbb{Z}\ \text{arbitrary} 操作後 A\subseteq B 條件：無 規則：forall_intro · 依賴：S02, S03, S06 葉節點依據：imp_intro + forall_intro + def_unfold 先依 →引入釋放 S03 的暫時假設，得 x∈A⇒x∈B；此後 x∈A 不再當作已知。S03 到 S06 對 x 只用到 x∈ℤ，沒有挑選特定的 x，所以依 ∀引入得 ∀x∈ℤ (x∈A⇒x∈B)；ℤ 以外的對象如 S02 所述自動成立。再依 S02 收回定義，得 A⊆B。 S08 · implies操作前 2=2\cdot 1,\quad 2\in A\iff\exists k\in\mathbb{Z},\ 6k=2 操作後 2\in B,\ 2\notin A 條件：無 規則：L_6k_ne_2 · 依賴：S01 葉節點依據：set_builder + exists_intro + quantifier_negation + int_discrete + order_basics 2=2·1 且 1∈ℤ，所以 2∈B。另一方面，依 A 的定義，2∈A 需要某個整數 k 使 6k=2；引理 L_6k_ne_2（在 S08.1、S08.2 證明）說沒有這樣的整數，依量詞否定，2∉A。 S09 · implies操作前 A\subseteq B,\ 2\in B,\ 2\notin A 操作後 A\neq B,\ A\subsetneq B 條件：無 規則：proper_subset_def · 依賴：S07, S08 葉節點依據：set_extensionality + proper_subset_def + and_intro_elim 依集合相等的判準，A=B 需要兩者有相同元素；2 在 B 中而不在 A 中，所以 A≠B。再加上 S07 的 A⊆B，依嚴格子集合定義得 A⊊B。嚴格性是另外證出的事實，不是 A⊆B 本身的含意。 S10 · equivalent操作前 B\subseteq B 操作後 \forall x\ (x\in B\Rightarrow x\in B) 條件：無 規則：mko_subset_def · 依賴：S01, mko_subset_def 葉節點依據：mko_subset_def + imp_intro + forall_intro 把同一定義用在兩個集合都是 B 的情形：B⊆B 等價於「對每個 x，x∈B⇒x∈B」。任何命題都蘊涵自己（假設 x∈B，結論 x∈B 就是這個假設），所以右邊成立，B⊆B 成立。這說明 ⊆ 是非嚴格包含：兩集合相等時包含仍成立，A⊆B 並不要求 A≠B。 S11 · equivalent操作前 \neg(A\subseteq C) 操作後 \exists x\ (x\in A\land x\notin C) 條件：無 規則：quantifier_negation · 依賴：S01, mko_subset_def 葉節點依據：mko_subset_def + quantifier_negation + neg_imp 要否定 A⊆C，先依定義寫成 ¬∀x (x∈A⇒x∈C)。依量詞否定得 ∃x ¬(x∈A⇒x∈C)，再依蘊涵的否定得 ∃x (x∈A ∧ x∉C)。所以否定包含只需要一個反例：A 中某個不屬於 C 的元素。 S12 · implies操作前 6=6\cdot 1,\quad 6\in C\iff\exists j\in\mathbb{Z},\ 4j=6 操作後 6\in A,\ 6\notin C 條件：無 規則：L_4j_ne_6 · 依賴：S01 葉節點依據：set_builder + exists_intro + quantifier_negation + int_discrete + order_basics 6=6·1 且 1∈ℤ，所以 6∈A。依 C 的定義，6∈C 需要某個整數 j 使 4j=6；引理 L_4j_ne_6（在 S12.1、S12.2 證明）說沒有這樣的整數，所以 6∉C。 S13 · implies操作前 6\in A\land 6\notin C 操作後 A\not\subseteq C 條件：無 規則：exists_intro · 依賴：S11, S12 葉節點依據：exists_intro + and_intro_elim + logic_chain 以 x=6 為見證：S12 給出 6∈A 且 6∉C，依 ∃引入得 ∃x (x∈A ∧ x∉C)；依 S11 的等價，A⊄C。一個反例就足以否定包含。 S14 · implies操作前 12=6\cdot 2,\ 12=4\cdot 3 操作後 12\in A\cap C\ \text{and yet}\ A\not\subseteq C 條件：無 規則：set_operations_def · 依賴：S01, S13 葉節點依據：set_builder + exists_intro + set_operations_def + numeric_evaluation 12=6·2 且 12=4·3，見證 2、3 都是整數，所以 12∈A 且 12∈C，即 12∈A∩C。但 S13 已證 A⊄C。所以找到共同元素並不能推出包含；包含是對 A 的每一個元素的要求。 S15 · equivalent操作前 \{6\}\subseteq A 操作後 6\in A 條件：無 規則：L_singleton_subset · 依賴：S12 葉節點依據：singleton_def + subset_def + forall_elim + forall_intro + eq_replace 依引理 L_singleton_subset（S=A，a=6），{6}⊆A 與 6∈A 同真同假；S12 已證 6∈A，所以 {6}⊆A 也成立。兩個語句真值相同，卻不是同一個語句：6∈A 比較一個元素與一個集合，{6}⊆A 比較兩個集合。 S16 · implies操作前 A\subseteq B,\ 2\in B\setminus A,\ 6\in A\setminus C,\ 6\in A 操作後 A\subsetneq B,\ A\not\subseteq C,\ B\subseteq B,\ \{6\}\subseteq A 條件：無 規則：and_intro_elim · 依賴：S07, S09, S10, S13, S14, S15 葉節點依據：and_intro_elim 彙整：A⊊B（S07、S09）；A⊄C，雖然 12∈A∩C（S13、S14）；B⊆B 顯示 ⊆ 允許相等（S10）；{6}⊆A 與 6∈A 同真，但型別角色不同（S15）。 ## 局部子步與引理 S08.1 · case_split操作前 k\in\mathbb{Z} 操作後 k\le 0\ \lor\ k\ge 1 條件：k\in\mathbb{Z} 規則：int_discrete · 依賴：int_discrete 葉節點依據：int_discrete + case_analysis 設 k 是任意整數。依整數的離散性（取 c=0），k≤0 或 k≥1，沒有第三種可能；兩種情況涵蓋所有整數。 S08.2 · implies操作前 k\le 0\ \lor\ k\ge 1 操作後 6k\neq 2 條件：6>0 規則：case_analysis · 依賴：S08.1, order_basics 葉節點依據：order_basics + case_analysis + forall_intro + numeric_evaluation 情況一：k≤0。兩邊乘以正數 6，得 6k≤0<2，所以 6k≠2。情況二：k≥1。兩邊乘以 6，得 6k≥6>2，所以 6k≠2。兩種情況都得 6k≠2，依分情況論證成立；k 是任意的，S08.1 與 S08.2 合起來證得引理 L_6k_ne_2。 S12.1 · case_split操作前 j\in\mathbb{Z} 操作後 j\le 1\ \lor\ j\ge 2 條件：j\in\mathbb{Z} 規則：int_discrete · 依賴：int_discrete 葉節點依據：int_discrete + case_analysis 設 j 是任意整數。依整數的離散性（取 c=1），j≤1 或 j≥2，兩種情況涵蓋所有整數。 S12.2 · implies操作前 j\le 1\ \lor\ j\ge 2 操作後 4j\neq 6 條件：4>0 規則：case_analysis · 依賴：S12.1, order_basics 葉節點依據：order_basics + case_analysis + forall_intro + numeric_evaluation 情況一：j≤1，乘以 4>0 得 4j≤4<6。情況二：j≥2，乘以 4 得 4j≥8>6。兩種情況都有 4j≠6；j 是任意的，S12.1 與 S12.2 合起來證得引理 L_4j_ne_6。 S15.1 · implies操作前 \{a\}\subseteq S 操作後 a\in S 條件：無 規則：forall_elim · 依賴：singleton_def, subset_def 葉節點依據：singleton_def + eq_refl_symm_trans + subset_def + forall_elim （⇒）依單元素集合定義，a∈{a}，因為 a=a。{a}⊆S 是說 {a} 的每個元素都在 S 中；把這個全稱語句代入 x=a（∀消去），得 a∈S。 S15.2 · implies操作前 a\in S 操作後 \{a\}\subseteq S 條件：無 規則：forall_intro · 依賴：singleton_def, subset_def 葉節點依據：singleton_def + eq_replace + imp_intro + forall_intro + subset_def （⇐）設 a∈S。取任意 x∈{a}；依單元素集合定義 x=a，依等值代換 x∈S。x 是任意的，依 ∀引入與子集合定義得 {a}⊆S。S15.1 與 S15.2 合起來證得引理 L_singleton_subset。 ## 逐步反向審查 - S16 · sufficient_goal_reduction · S07, S09, S10, S13, S14, S15, and_intro_elim — 目標 G 是題目各結論的合取；每一項都由所列步驟正向證成，此步只做合取，沒有把 G 當作前提。 - S15.2 · premise_audit · singleton_def, eq_replace, forall_intro, subset_def — 這一步只證 ⇐ 方向；與 S15.1 合起來才是等價。除了 x∈{a}，對 x 沒有其他假設。 - S15.1 · premise_audit · singleton_def, subset_def, forall_elim, eq_refl_symm_trans — 需要 a∈{a}，由等號的自反性 a=a 得到。這一步只證 ⇒ 方向。 - S15 · inverse_equivalence · L_singleton_subset — 引理的兩個方向分別在 S15.1、S15.2 證明，所以等價雙向成立。 - S14 · premise_audit · S13, set_builder, set_operations_def, exists_intro — 此步只證明一個共同元素存在，並與 S13 並列；不宣稱共同元素推出任何包含關係。 - S13 · sufficient_goal_reduction · S11, S12, exists_intro — 目標 G：A⊄C。足夠條件 H：存在 x 使 x∈A 且 x∉C；H⇒G 由 S11。H 由 S12 的具體見證正向證成，沒有把 G 當作前提。 - S12.2 · premise_audit · S12.1, order_basics, case_analysis, forall_intro — 需要 4>0 才能保持不等號方向；只推出 4j≠6，不宣稱反向。 - S12.1 · premise_audit · int_discrete — 對實數不窮盡：j=3/2 恰好使 4j=6（N13），所以必須用到 j 是整數。 - S12 · premise_audit · L_4j_ne_6, set_builder, exists_intro, quantifier_negation — 與 S08 相同：屬於只需一個見證，不屬於必須排除所有整數 j。 - S11 · inverse_equivalence · mko_subset_def, quantifier_negation, neg_imp — 三個改寫（定義、量詞否定、蘊涵的否定）都是等價，所以整步雙向成立。 - S10 · inverse_equivalence · mko_subset_def, imp_intro — 與 S02 相同，定義是雙向的；右邊的全稱語句由 →引入直接成立。 - S09 · premise_audit · S07, S08, set_extensionality, proper_subset_def — A⊊B 需要兩件事：A⊆B（S07）與 A≠B（S08 的見證 2）。只有前者不足以得到嚴格包含。 - S08.2 · premise_audit · S08.1, order_basics, case_analysis, forall_intro — 乘以 6 保持不等號方向，需要 6>0。結論是單向的：只推出 6k≠2，不宣稱其他。 - S08.1 · premise_audit · int_discrete — 分情況必須窮盡；對實數這兩種情況並不窮盡（例如 k=1/3，而 6·(1/3)=2），所以這裡必須用到 k 是整數。 - S08 · premise_audit · L_6k_ne_2, set_builder, exists_intro, quantifier_negation — 2∈B 只需一個見證；2∉A 必須排除所有整數 k，這正是引理提供的全稱語句。只試 k=0、1 並不夠，所以引理用分情況涵蓋所有整數。 - S07 · sufficient_goal_reduction · S02, S06, imp_intro, forall_intro — 目標 G：A⊆B。足夠條件 H：對任意 x∈ℤ，x∈A⇒x∈B；H⇒G 由 S02 的等價。H 由 S03 到 S06 從定義正向證成，x 是任意的，沒有把 G 當作前提。 - S06 · premise_audit · S05, int_closure, exists_intro, set_builder — 關鍵是見證 m=3k₀ 確實是整數。若見證不是整數（例如 3=2·(3/2)），就不能推出屬於 B。反向 x∈B⇒x∈A 不宣稱：2∈B 但 2∉A（S08）。 - S05 · inverse_equivalence · mul_assoc, numeric_evaluation, eq_replace — 反向：2(3k₀)=(2·3)k₀=6k₀，回到 x=6k₀；以相等的式子代換，雙向成立。 - S04 · premise_audit · S03, exists_elim — 需要 S03 的存在語句，且 k₀ 是新名字、不出現在結論中。不宣稱 k₀ 是唯一的這種整數（事實上唯一，但本稿不需要）。 - S03 · inverse_equivalence · set_builder — 集合建構式的成員條件是雙向的：有這樣的 k 就推出 x∈A，x∈A 也提供這樣的 k。 - S02 · inverse_equivalence · mko_subset_def, subset_def — MKO 的定義是「當且僅當」，展開與收回兩個方向都由定義保證。 - S01 · premise_audit · G1, G2, def_intro, set_builder — 此步只命名，不推出新事實。它核對的是前提：三個集合都從 ℤ 取元素，所以論域相同。 ## 錯誤控制與反例 只檢查部分元素不夠MKO 指出常見誤解是只檢查部分元素就斷言包含。12 同屬 A 與 C，但 A⊄C（6∈A∖C）。同樣地，驗證 6、12、18、24、30 都是偶數，只說明這五個元素屬於 B，並不證明 A⊆B；本稿的證明從任意的 x∈A 出發（S03 到 S07），用到的只有 x=6k₀ 與恆等式 6k₀=2(3k₀)，所以涵蓋 A 的每一個元素。 ⊆ 是非嚴格包含另一個誤解是認為 A⊆B 必須 A≠B。S10 證明 B⊆B 成立，所以 ⊆ 允許兩集合相等。若要說嚴格包含 A⊊B，必須另外證明 A≠B，本稿在 S08、S09 以見證 2∈B∖A 完成；不能從 A⊆B 直接讀出。 x∈A 與 {x}⊆A 不是同一語句MKO 提醒不要把 x∈A 與 {x}⊆A 混為同一語句。S15 證明兩者等價（同真同假），但型別角色不同：6∈A 的左邊是整數，{6}⊆A 的左邊是整數集合。寫成 6⊆A 是型別錯誤（6 不是集合）；在 Lean 的 Set ℤ 中，{6}∈A 也不是合法語句，因為 A 的元素是整數而不是整數集合。 - 12∈A 且 12∈C，所以 A⊆C → reject — 包含要求 A 的每個元素都在 C 中；6∈A 但 6∉C（S12、S13）。 - 6、12、18、24、30 都是偶數，所以 A⊆B 已被證明 → reject — 結論雖然為真，但有限個例子不證明全稱語句；證明需要從任意 x∈A 出發（S03 到 S07）。 - A⊆B 要求 A≠B，所以 B⊆B 不成立 → reject — ⊆ 是非嚴格包含；S10 證明 B⊆B 成立。 - 6∈B 且 6∈A，所以 B⊆A → reject — 2∈B 但 2∉A（S08），所以 B⊄A。 - 6∈A 與 6⊆A 是同一個語句 → reject — 6 是元素不是集合，6⊆A 型別不合；與 6∈A 等價的是 {6}⊆A，而且兩者仍是不同語句。 ## 結論與限制 在論域 ℤ 中，6 的倍數之集 A 是偶數之集 B 的子集合，而且是嚴格子集合（2∈B∖A）；A 不是 4 的倍數之集 C 的子集合（6∈A∖C），雖然 12 同屬兩者；B⊆B 說明 ⊆ 允許相等；{6}⊆A 與 6∈A 等價，但是不同的語句。 - 整數的乘法封閉性與離散性（int_closure、int_discrete）是前置知識，本稿不從整數公理推出。 - N10 只在 k=−20 到 20 的範圍內核對 6k≠2，是有限檢查，不證明全稱語句；全稱語句由 S08.1、S08.2 證明。N11、N12 以餘數做的交叉核對只對這兩個數有效，論證不依賴它們。 ## 驗證及來源綁定 14 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 88bf090b03281e737b94f71d45f7b57b3e7962272b65b9b44ff45256ac8be3a0 - original source SHA-256: 88bf090b03281e737b94f71d45f7b57b3e7962272b65b9b44ff45256ac8be3a0 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-subset-01.json)