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

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-set-membership/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-set-membership-01 · production-20261019-adopted-96



## 目標與範圍

在型別化語境中，設 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





## 逐步主鏈

S01 · definition操作前

x,\ A

操作後

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

條件：無

規則：mko_member · 依賴：G1, G2

葉節點依據：mko_member + list_set

依 MKO，給定集合 A 與對象 x，x∈A 是一個命題：它斷言 x 是 A 的元素，可能為真也可能為假。它不表示 x 等於 A，也不表示 x 是 A 的子集合。MKO 也記錄：在目前的 Lean 映射中，Set α 表示為 α→Prop，所以 x∈A 與「A x」在定義上等價；也就是說，集合由「對每個 x 給出一個命題」決定。本稿不執行 Lean，只採用這個觀點。



S02 · implies操作前

2\in A

操作後

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

條件：無

規則：list_set · 依賴：S01, G2, list_set

葉節點依據：list_set + eq_refl_symm_trans

依列舉記號，2∈A ⇔ 2=1 ∨ 2=2 ∨ 2=3。第二支 2=2 依等號的反身性成立，所以析取為真，2∈A 為真。



S03 · implies操作前

4\in A

操作後

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

條件：無

規則：de_morgan_logic · 依賴：G2, list_set

葉節點依據：de_morgan_logic + list_set + numeric_evaluation

依列舉記號 4∈A ⇔ 4=1 ∨ 4=2 ∨ 4=3。三個等式都不成立，依德摩根律 ¬(4=1∨4=2∨4=3) ⇔ 4≠1∧4≠2∧4≠3，所以 4∉A。「4∈A」仍是一個命題，只是假的。



S04 · equivalent操作前

B\subseteq A

操作後

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

條件：無

規則：subset_def · 依賴：G2

葉節點依據：subset_def + def_unfold

依子集定義展開：B⊆A 表示 B 的每個元素都是 A 的元素。注意 ⊆ 談的是 B 的元素，∈ 談的是單一對象。



S05 · case_split操作前

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

操作後

x=1\ \lor\ x=2

條件：無

規則：list_set · 依賴：S04, G2, list_set

葉節點依據：list_set + case_analysis

任取整數 x 並暫時假設 x∈B。依列舉記號 x=1 或 x=2，兩支涵蓋 x∈B 的所有可能，在 S05.1、S05.2 處理。



S06 · implies操作前

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

操作後

B\subseteq A

條件：無

規則：forall_intro · 依賴：S04, S05, S05.1, S05.2

葉節點依據：case_analysis + imp_intro + forall_intro

兩支都推出 x∈A，依分情況論證，在假設 x∈B 下得 x∈A；釋放假設得 x∈B ⇒ x∈A。x 是任取的，依全稱推廣與 S04，B⊆A。



S07 · implies操作前

3\in A,\ 3\notin B

操作後

A\not\subseteq B

條件：無

規則：quantifier_negation · 依賴：G2, list_set

葉節點依據：quantifier_negation + exists_intro + list_set + numeric_evaluation

3∈A（第三支 3=3）；3∈B ⇔ 3=1 ∨ 3=2，兩者都不成立，所以 3∉B。於是 ∃x (x∈A ∧ x∉B)，依量詞否定 ¬∀x (x∈A ⇒ x∈B)，即 A⊄B。⊆ 不是對稱的。



S08 · implies操作前

B\in\mathcal{F}

操作後

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

條件：無

規則：list_set · 依賴：G1, G2, list_set

葉節點依據：list_set + typed_membership + eq_refl_symm_trans

𝓕 的元素是整數的集合，B 也是整數的集合，所以 B∈𝓕 是良構命題。依列舉記號，B∈𝓕 ⇔ B={1,2} ∨ B={3}；B 就是 {1,2}（等號的反身性），所以 B∈𝓕 為真。這是 B 作為一個整體是 𝓕 的元素，與 B⊆A（B 的每個元素都在 A 中）是不同的關係。



S09 · implies操作前

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

操作後

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

條件：無

規則：set_extensionality · 依賴：G2, list_set, set_extensionality

葉節點依據：set_extensionality + list_set + de_morgan_logic + numeric_evaluation

{1}∈𝓕 ⇔ {1}={1,2} ∨ {1}={3}。2∈{1,2} 而 2∉{1}（2≠1），依外延性 {1}≠{1,2}；1∈{1} 而 1∉{3}（1≠3），所以 {1}≠{3}。兩支都假，{1}∉𝓕。可是 {1}⊆B 而且 B∈𝓕：隸屬於 𝓕 不會傳給子集合。



S10 · implies操作前

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

操作後

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

條件：無

規則：typed_membership · 依賴：S08, G1, typed_membership

葉節點依據：typed_membership

1∈B 為真（第一支 1=1），B∈𝓕 為真（S08）。但 𝓕 的元素是整數的集合，1 是整數，依 typed_membership，「1∈𝓕」在型別化的讀法中不是良構命題，更不是真命題；若改用不分型別的讀法，它表示 1={1,2} 或 1={3}，在把整數與這兩個集合視為不同對象時也不成立。所以 ∈ 沒有傳遞性：x∈B 與 B∈𝓕 不推出 x∈𝓕。



S11 · implies操作前

1000000\in E

操作後

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

條件：無

規則：set_builder · 依賴：G2, set_builder, divides_def

葉節點依據：set_builder + divides_def + exists_intro + numeric_evaluation

依建構式，1000000∈E ⇔ 1000000∈ℤ 且 2∣1000000。1000000=2·500000，500000 是整數，所以 2∣1000000，1000000∈E 為真。這個判定只用 E 的定義條件，不需要把 E 的元素列出或存放在任何容器裡。



S12 · case_split操作前

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

操作後

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

條件：k\in\mathbb{Z}

規則：int_no_gap · 依賴：G2

葉節點依據：int_no_gap + case_analysis

7∈E 需要 2∣7，即整數 k 使 7=2k。依 int_no_gap（m=3），每個整數 k 滿足 k≤3 或 k≥4，兩支在 S12.1、S12.2 處理。



S13 · implies操作前

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

操作後

7\notin E

條件：無

規則：case_analysis · 依賴：S12, S12.1, S12.2, G2, set_builder

葉節點依據：case_analysis + set_builder + divides_def

兩支都得 2k≠7，所以沒有整數 k 使 7=2k，即 2∤7；依建構式 7∈E ⇔ 2∣7，因此 7∉E。「7∈E」是一個假的命題。



S14 · implies操作前

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

操作後

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

條件：無

規則：python_in · 依賴：python_in, list_set

葉節點依據：python_in + list_set

依引用的 Python 語言參考（python_in），對字串而言 x in y 是子字串測試，所以 '12' in '123' 為 True。若把 '123' 的三個字元看成由單字元字串組成的集合 {'1','2','3'}，則 '12'∈{'1','2','3'} ⇔ '12'='1' ∨ '12'='2' ∨ '12'='3'；'12' 有兩個字元，與三個單字元字串都不相等，所以這是假命題。同一個「in」在程式中檢查的是另一種關係；MKO 提醒不要把程式容器的成員測試當作集合隸屬的全部語義。



S15 · implies操作前

\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

條件：無

規則：and_intro_elim · 依賴：S02, S03, S06, S07, S08, S09, S10, S11, S13, S14

葉節點依據：and_intro_elim

合起來：2∈A 真、4∈A 假、B⊆A 真、A⊆B 假、B∈𝓕 真、{1}∈𝓕 假、1000000∈E 真、7∈E 假；1∈B 與 B∈𝓕 不給出 1∈𝓕；程式的字串成員測試與集合隸屬是不同關係。







## 局部子步與引理

S05.1 · implies操作前

x=1

操作後

x\in A\ \ (1=1)

條件：無

規則：list_set · 依賴：S05, list_set

葉節點依據：list_set + eq_replace

若 x=1，則 x∈A ⇔ 1=1 ∨ 1=2 ∨ 1=3，第一支成立，所以 x∈A。



S05.2 · implies操作前

x=2

操作後

x\in A\ \ (2=2)

條件：無

規則：list_set · 依賴：S05, list_set

葉節點依據：list_set + eq_replace

若 x=2，依 S02，x∈A。



S12.1 · implies操作前

k\le 3

操作後

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

條件：2>0

規則：order_basics · 依賴：S12

葉節點依據：order_basics + numeric_evaluation

若 k<3，乘以正數 2 得 2k<6；若 k=3，2k=6。所以 2k≤6<7，2k≠7。



S12.2 · implies操作前

k\ge 4

操作後

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

條件：2>0

規則：order_basics · 依賴：S12

葉節點依據：order_basics + numeric_evaluation

若 k>4，乘以 2 得 2k>8；若 k=4，2k=8。所以 2k≥8>7，2k≠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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-set-membership-01.json)