集合隸屬：x∈A 是命題，並與 ⊆、= 及程式的成員測試區分

目標與範圍

在型別化語境中，設 A={1,2,3}、B={1,2}、𝓕={{1,2},{3}}（元素是整數集合的集合）、E={n∈ℤ ∣ 2∣n}。判定下列命題的真假並給出理由：2∈A；4∈A；B⊆A；A⊆B；B∈𝓕；{1}∈𝓕；1000000∈E；7∈E。並說明 1∈B 與 B∈𝓕 為何不給出 1∈𝓕，以及程式語言的成員測試為何不能取代集合隸屬的語義。

依 MKO：給定集合 A 與對象 x，x∈A 是一個命題，表示 x 是 A 的元素。在型別化語境中處理整數的集合與整數集合的集合，只用列舉式與建構式集合。不建立集合論公理，不展開 Lean 映射的細節（MKO 第三段只作說明）；不改動 canonical MKO 或英文 edition。

已知條件與符號

• subset_def
• set_extensionality
• set_builder
• divides_def
• order_basics
• numeric_evaluation

• G1 — 型別化語境：對象是整數；A、B、E 是整數的集合；𝓕 是整數集合的集合。x∈S 只在 x 的型別與 S 的元素型別相同時才是良構命題。列舉記號：x∈{a,b,c} ⇔ x=a ∨ x=b ∨ x=c（兩個或一個元素時同理）；對集合的列舉同樣適用，此時等號是集合相等。
• G2 — A={1,2,3}，B={1,2}，𝓕={{1,2},{3}}，E={n∈ℤ ∣ 2∣n}。

• x\in A — x 是 A 的元素（一個命題）
• B\subseteq A — B 的每個元素都是 A 的元素
• \mathcal{F} — 元素是整數集合的集合
• E=\{n\in\mathbb{Z}\mid 2\mid n\} — 以條件給出的偶數集合
• \{1\} — 只含 1 的集合

規則與來源

• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
• 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 — 明確整數或有理數算式的精確求值；可以獨立重算。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• imp_intro · prerequisite — →引入（釋放假設）：若在暫時假設 P 的作用域中推出 Q，則得到 P⇒Q；此後 P 不再可當作已知使用。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_member · cited — 給定集合 A 與對象 x，x∈A 是一個命題，表示 x 是 A 的元素。 · mko-set-membership
• list_set · prerequisite — 列舉式集合：x∈{a,b,c} ⇔ x=a ∨ x=b ∨ x=c；兩個或一個元素時同理。
• typed_membership · prerequisite — 型別化的隸屬：x∈S 只在 x 的型別是 S 的元素型別時才是良構命題；整數不是整數的集合，整數的集合也不是整數。
• int_no_gap · prerequisite — 整數沒有空隙：對整數 k 與 m，必有 k≤m 或 k≥m+1。
• python_in · cited — 對字串型別，x in y 為 True 當且僅當 x 是 y 的子字串；因此 '12' in '123' 的值為 True。 · Python Software Foundation, Python Language Reference, Section 6.10.2 Membership test operations

逐步主鏈

x,\ A

x\in A\ \text{is a proposition: }x\ \text{is an element of}\ A

2\in A

2=1\lor 2=2\lor 2=3:\ \text{true, since}\ 2=2

4\in A

4\neq 1\land 4\neq 2\land 4\neq 3,\ \text{so}\ 4\notin A

B\subseteq A

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

x\in B\ (x\ \text{arbitrary})

x=1\ \lor\ x=2

x\in B\Rightarrow x\in A\ \text{for arbitrary}\ x

B\subseteq A

3\in A,\ 3\notin B

A\not\subseteq B

B\in\mathcal{F}

B=\{1,2\}\lor B=\{3\}:\ \text{true}

\{1\}\in\mathcal{F}

\{1\}\neq\{1,2\},\ \{1\}\neq\{3\},\ \text{so}\ \{1\}\notin\mathcal{F}

1\in B,\ B\in\mathcal{F}

1\in\mathcal{F}\ \text{is not a true statement}

1000000\in E

1000000=2\cdot 500000,\ \text{so}\ 1000000\in E

k\in\mathbb{Z}\ \text{with}\ 2k=7\ ?

k\le 3\ \lor\ k\ge 4

\forall k\in\mathbb{Z}:\ 2k\neq 7

7\notin E

\text{Python: }'12'\ \text{in}\ '123'

\text{True (substring test), while}\ '12'\notin\{'1','2','3'\}

\text{verdicts of S02 to S14}

2\in A,\ 4\notin A,\ B\subseteq A,\ A\not\subseteq B,\ B\in\mathcal{F},\ \{1\}\notin\mathcal{F},\ 1000000\in E,\ 7\notin E

局部子步與引理

x=1

x\in A\ \ (1=1)

x=2

x\in A\ \ (2=2)

k\le 3

2k\le 6<7,\ \text{so}\ 2k\neq 7

k\ge 4

2k\ge 8>7,\ \text{so}\ 2k\neq 7

逐步反向審查

• S15 · sufficient_goal_reduction · S02, S03, S06, S07, S08, S09, S10, S11, S13, S14, and_intro_elim — 目標 G：題目要求的各項判定與說明。足夠條件 H：所列各步結論；H⇒G 只是並列。H 由 G1、G2 與引用規則正向證成，沒有把 G 當作前提。
• S14 · premise_audit · python_in, list_set — 程式行為來自引用的語言參考（citation_verified，本稿沒有執行程式）；集合一側只用列舉記號。不宣稱所有程式語言或所有容器型別都如此。
• S13 · premise_audit · S12, case_analysis, set_builder, divides_def — 需要兩支涵蓋全部整數（S12）。
• S12.2 · premise_audit · order_basics — 同 S12.1。
• S12.1 · premise_audit · order_basics, two_nonzero — 用到 2>0；不宣稱反向。
• S12 · premise_audit · int_no_gap — 兩支涵蓋全部整數。
• S11 · premise_audit · set_builder, divides_def, exists_intro, numeric_evaluation — 需要一個整數見證 500000（N8）。
• S10 · premise_audit · typed_membership, S08 — 結論依賴型別區分；不分型別時的判定另需數的編碼，本稿不處理。
• S09 · premise_audit · set_extensionality, list_set, de_morgan_logic — 每個集合不等式各需一個只屬於一邊的元素；兩支都否定後析取為假。
• S08 · premise_audit · list_set, typed_membership, eq_refl_symm_trans — 需要型別相符（B 是整數集合）與一支為真。
• S07 · premise_audit · list_set, quantifier_negation, exists_intro — 一個反例就足以否定子集關係。
• S06 · sufficient_goal_reduction · S04, S05, case_analysis, imp_intro, forall_intro — 目標 G：B⊆A。足夠條件 H：∀x (x∈B⇒x∈A)；H⇒G 由 S04。H 由 S05 及其子步正向證成。
• S05.2 · premise_audit · list_set, S02, eq_replace — 直接引用 S02。
• S05.1 · premise_audit · list_set, eq_replace — 用 x=1 代換後只需一支為真。
• S05 · premise_audit · list_set, imp_intro — 列舉記號給出完整的分支；暫時假設在 S06 釋放。
• S04 · inverse_equivalence · subset_def — 展開與收回定義是雙向的。
• S03 · premise_audit · list_set, de_morgan_logic, numeric_evaluation — 要否定析取，必須每一支都不成立（N1 到 N3）。
• S02 · premise_audit · list_set, eq_refl_symm_trans — 析取只需一支為真。
• S01 · premise_audit · G1, G2, mko_member — 此步只寫出定義與型別，不推出新事實。

錯誤控制與反例

隸屬與子集合是兩種關係

MKO 指出常見誤解是混淆 x∈A 與 B⊆A。本稿中 B⊆A（S06）但 B 不是 A 的元素；B∈𝓕（S08）而 {1}⊆B，{1} 卻不是 𝓕 的元素（S09）；1∈B、B∈𝓕 也不推出 1∈𝓕（S10）。∈ 連接一個對象與一個集合，⊆ 連接兩個同型別的集合，兩者的推理規則不同。

程式的成員測試不是集合語義

MKO 的另一個誤解是把程式容器的成員測試當作所有集合論語義。依引用的 Python 參考，字串的 in 是子字串測試，'12' in '123' 為 True，但作為集合 '12'∈{'1','2','3'} 為假（S14）。用程式核對集合命題前，必須先確認該運算子的語義與 ∈ 一致。

x∈A 是命題，可以為假

4∈A 與 7∈E 都是假的命題（S03、S13），它們仍是命題。E 以條件給出，判定 1000000∈E 只需檢查條件（S11），不必把 E 的元素列出或存放：集合不必依靠實際的容器而存在（MKO 第一段）。

• 因為 B⊆A，所以 B∈A → reject — A 的元素是 1、2、3 這些整數；B 是集合，不是其中任何一個（在型別化讀法中 B∈A 甚至不是良構的）。
• 1∈B 且 B∈𝓕，所以 1∈𝓕 → reject — ∈ 沒有傳遞性；𝓕 的元素是集合 {1,2} 與 {3}，1 不是其中之一（S10）。
• {1}⊆{1,2} 且 {1,2}∈𝓕，所以 {1}∈𝓕 → reject — {1} 不等於 {1,2} 也不等於 {3}（S09）。
• Python 中 '12' in '123' 為 True，所以作為集合 '12'∈{'1','2','3'} → reject — 字串的 in 是子字串測試；'12' 不等於任何一個單字元字串（S14）。

結論與限制

2∈A 為真，4∈A 為假（仍是命題）；B⊆A 為真而 A⊆B 為假（3∈A、3∉B）；B∈𝓕 為真，{1}∈𝓕 為假，儘管 {1}⊆B；1000000∈E 為真（1000000=2·500000），7∈E 為假。1∈B 與 B∈𝓕 不推出 1∈𝓕，因為 ∈ 沒有傳遞性，而且在型別化語境中「1∈𝓕」不是良構命題。Python 的 '12' in '123' 為 True 是子字串測試，而 '12'∈{'1','2','3'} 為假：程式的成員測試不是集合隸屬的語義。

• python_in 的字串成員測試語義已核對 Python 官方語言參考；這是文件核查，不宣稱稿件中的程式已實際執行。
• 本稿以型別化語境為前提（typed_membership）；不分型別的集合論中 1∈𝓕 的判定依賴數的編碼，本稿不處理。

驗證及來源綁定

11 個本稿宣告算術檢查；只支持所列算式。

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 6dd4b8c91e6e6cf5db9b127bce6c4343aa4499b9a88cd0668513c03caa224cfb
• original source SHA-256: 6dd4b8c91e6e6cf5db9b127bce6c4343aa4499b9a88cd0668513c03caa224cfb
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）