子集合：以任意元素證明包含，並以反例否定包含

目標與範圍

在論域 ℤ 中，令 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 — 實數的序：任兩數恰有 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。
• 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。

逐步主鏈

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

A\subseteq B

\forall x\ (x\in A\Rightarrow x\in B)

x\in A\ \ (x\in\mathbb{Z}\ \text{arbitrary})

\exists k\in\mathbb{Z},\ x=6k

\exists k\in\mathbb{Z},\ x=6k

x=6k_0,\ k_0\in\mathbb{Z}

x=6k_0

x=2(3k_0)

x=2(3k_0),\ k_0\in\mathbb{Z}

x\in B

x\in A\ \text{assumed}\ \vdash\ x\in B,\quad x\in\mathbb{Z}\ \text{arbitrary}

A\subseteq B

2=2\cdot 1,\quad 2\in A\iff\exists k\in\mathbb{Z},\ 6k=2

2\in B,\ 2\notin A

A\subseteq B,\ 2\in B,\ 2\notin A

A\neq B,\ A\subsetneq B

B\subseteq B

\forall x\ (x\in B\Rightarrow x\in B)

\neg(A\subseteq C)

\exists x\ (x\in A\land x\notin C)

6=6\cdot 1,\quad 6\in C\iff\exists j\in\mathbb{Z},\ 4j=6

6\in A,\ 6\notin C

6\in A\land 6\notin C

A\not\subseteq C

12=6\cdot 2,\ 12=4\cdot 3

12\in A\cap C\ \text{and yet}\ A\not\subseteq C

\{6\}\subseteq A

6\in A

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

局部子步與引理

k\in\mathbb{Z}

k\le 0\ \lor\ k\ge 1

k\le 0\ \lor\ k\ge 1

6k\neq 2

j\in\mathbb{Z}

j\le 1\ \lor\ j\ge 2

j\le 1\ \lor\ j\ge 2

4j\neq 6

\{a\}\subseteq S

a\in S

a\in S

\{a\}\subseteq S

逐步反向審查

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