# 事件：在完整事件族與較粗事件族中判定事件

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

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

derivation-mko-event-01 · production-20261019-adopted-96



## 目標與範圍

擲一顆骰子一次，S={1,2,3,4,5,6}。(1) 在有限初等模型 F=𝒫(S) 中，說明 E={2,4,6} 是事件，判定觀察結果為 4 與 3 時 E 是否發生；分辨結果 4 與事件 {4}；說明空事件與必然事件。(2) 在一般模型 (S,F₀) 中，F₀={∅,O,E,S}，O={1,3,5}：證明 F₀ 是 S 上的事件族（σ-代數），並證明 {6}∉F₀，所以雖然 S 有限且 {6}⊆S，{6} 在這個模型中不是事件。

在 MKO 的範圍內工作：樣本空間 S 明示（假設 a1），兩個模型的事件族都明示（假設 a2）。一般模型的事件族採用標準的 σ-代數定義（前置知識 sigma_algebra_def）。不指派任何機率值；不處理無限樣本空間或 Lean 的 MeasurableSet；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- subset_def
- set_operations_def
- set_extensionality
- powerset_def
- sigma_algebra_def


- G1 — 試驗：擲一顆六面骰一次，記錄朝上的點數；樣本空間 S={1,2,3,4,5,6}（假設 a1）。
- G2 — 模型 M1：有限初等模型，明示事件族 F=𝒫(S)（假設 a2）。
- G3 — 模型 M2：一般模型 (S,F₀)，明示 F₀={∅,O,E,S}，其中 O={1,3,5}、E={2,4,6}（例如只能觀察點數奇偶的情形）（假設 a2）。


- S — 擲骰一次的樣本空間
- \mathcal{P}(S) — S 的所有子集合構成的完整事件族
- F_0 — 較粗的事件族 {∅,O,E,S}
- E,\ O — 偶數結果之集、奇數結果之集
- \omega — 觀察到的結果
- S\setminus X — X 在 S 中的補集





## 規則與來源


- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- 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。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_event_def · cited — 本條目的有限初等模型明示採完整事件族 F=P(S)，因此事件 E 可取 S 的任一子集合；一般指定為 (S,F) 的模型不論 S 有限或無限，都要求事件 E 屬於 F。試驗結果屬於 E 時稱事件 E 發生。 · mko-event
- powerset_def · prerequisite — 冪集：X∈𝒫(S) 當且僅當 X⊆S。
- sigma_algebra_def · prerequisite — 事件族（σ-代數）：S 的子集合族 F 稱為 S 上的事件族，若 S∈F；X∈F 時 S∖X∈F；且 F 中任意可數多個（含有限多個）成員的聯集都屬於 F。
- L_F0_unions · lemma — F₀ 中任意可數多個成員的聯集仍屬於 F₀。





## 逐步主鏈

S01 · definition操作前

\text{one roll of a die}

操作後

S=\{1,2,3,4,5,6\},\ E=\{2,4,6\},\ O=\{1,3,5\}

條件：無

規則：def_intro · 依賴：G1, G2, G3

葉節點依據：def_intro + mko_event_def

先明示樣本空間 S，再為兩個要用到的子集合取名：E 是偶數結果，O 是奇數結果。依 MKO，列事件之前必須先指定樣本空間與事件族；兩個模型的事件族由 G2、G3 明示。



S02 · implies操作前

E=\{2,4,6\},\ O=\{1,3,5\}

操作後

E\subseteq S,\ O\subseteq S

條件：無

規則：subset_def · 依賴：S01

葉節點依據：subset_def + forall_intro

E 的三個元素 2、4、6 都在 S 中，O 的三個元素 1、3、5 也都在 S 中；這檢查了這兩個有限集合的全部元素，所以依子集合定義 E⊆S、O⊆S。



S03 · equivalent操作前

E\subseteq S

操作後

E\in\mathcal{P}(S)=F

條件：F=\mathcal{P}(S)

規則：powerset_def · 依賴：G2, S02

葉節點依據：powerset_def + eq_replace

在模型 M1 中 F=𝒫(S)。依冪集定義，X∈𝒫(S) 當且僅當 X⊆S；由 S02，E⊆S，所以 E∈F，E 是 M1 中的事件。依 MKO，只有明示採用 F=𝒫(S) 時，才可以這樣由「是子集合」直接得到「是事件」。



S04 · implies操作前

\omega=4,\quad \omega=3

操作後

4\in E\Rightarrow E\ \text{occurs};\quad 3\notin E\Rightarrow E\ \text{does not occur}

條件：E\in F

規則：mko_event_def · 依賴：S01, S03

葉節點依據：mko_event_def + def_unfold

依 MKO，試驗結果屬於 E 時稱 E 發生。觀察到 ω=4 時，4 是 E 列舉中的一個，所以 E 發生；觀察到 ω=3 時，3 不在 {2,4,6} 中，所以 E 不發生。事件是否發生，由觀察結果是否屬於它決定。



S05 · implies操作前

4\in S,\ \{4\}\subseteq S

操作後

4\ \text{is an outcome},\ \{4\}\in F,\ 4\neq\{4\}

條件：F=\mathcal{P}(S)

規則：powerset_def · 依賴：S01, S03

葉節點依據：powerset_def + subset_def + mko_event_def

4 是 S 的元素，是一個基本結果；{4} 是 S 的子集合，在 M1 中依冪集定義屬於 F，是一個事件。兩者型別不同：4 是數，{4} 是集合，4≠{4}。觀察到結果 4 時，事件 {4} 發生；E={2,4,6} 含三個結果，所以事件一般不是單一結果。



S06 · implies操作前

\varnothing\subseteq S,\ S\subseteq S

操作後

\varnothing,\ S\in F;\ \varnothing\ \text{never occurs},\ S\ \text{always occurs}

條件：F=\mathcal{P}(S)

規則：powerset_def · 依賴：S01, G2

葉節點依據：powerset_def + subset_def + mko_event_def

∅⊆S（沒有元素需要檢查），S⊆S，所以在 M1 中兩者都是事件。沒有任何 ω 屬於 ∅，所以空事件從不發生；每個觀察結果都屬於 S（樣本空間包含所有可能結果），所以必然事件 S 總是發生。這些名稱並沒有指派機率值。



S07 · implies操作前

F_0=\{\varnothing,O,E,S\}

操作後

F_0\subseteq\mathcal{P}(S),\ S\in F_0

條件：無

規則：sigma_algebra_def · 依賴：G3, S02, S06

葉節點依據：sigma_algebra_def + subset_def

進入模型 M2，依 σ-代數定義逐條核對。第一條：F₀ 的四個成員 ∅、O、E、S 都是 S 的子集合（S02、S06），所以 F₀ 是 S 的子集合族；而且 S 是 F₀ 的成員之一。



S08 · implies操作前

S\setminus\varnothing,\ S\setminus S,\ S\setminus E,\ S\setminus O

操作後

S,\ \varnothing,\ O,\ E\ \in F_0

條件：無

規則：set_operations_def · 依賴：S07

葉節點依據：set_operations_def + set_extensionality

逐一計算 F₀ 每個成員在 S 中的補集：S∖∅=S，S∖S=∅；S∖E 是 S 中不屬於 {2,4,6} 的元素，即 {1,3,5}=O；同理 S∖O=E。四個補集都在 F₀ 中，所以 F₀ 對補集封閉，σ-代數的第二條成立。



S09 · implies操作前

E=\{2,4,6\},\ O=\{1,3,5\}

操作後

E\cup O=S,\ E\cap O=\varnothing

條件：無

規則：set_operations_def · 依賴：S01

葉節點依據：set_operations_def + set_extensionality + numeric_evaluation

S 的六個元素中，2、4、6 在 E，1、3、5 在 O，每個元素恰好屬於其中一個。所以 E∪O=S 且 E∩O=∅；個數核對 3+3=6。之後稱 E、O 為 F₀ 的原子。



S10 · implies操作前

(X_i)_{i\in\mathbb{N}}\ \text{with each}\ X_i\in F_0

操作後

\bigcup_{i\in\mathbb{N}}X_i\in F_0;\ F_0\ \text{is an event family on }S

條件：無

規則：L_F0_unions · 依賴：S07, S08, S09

葉節點依據：sigma_algebra_def + set_operations_def + case_analysis + exists_elim

依引理 L_F0_unions（在 S10.1 到 S10.3 證明），F₀ 中任意可數多個成員的聯集仍在 F₀ 中；有限聯集是特例（其餘各項取 ∅）。連同 S07、S08，σ-代數定義的三條都成立，所以 F₀ 是 S 上的事件族，M2 是合法的一般模型。



S11 · implies操作前

\{6\}\ \text{compared with}\ \varnothing,\ O,\ E,\ S

操作後

\{6\}\notin F_0

條件：無

規則：set_extensionality · 依賴：S01, G3

葉節點依據：set_extensionality + case_analysis

{6} 要屬於 F₀，必須等於四個成員之一。{6}≠∅，因為 6∈{6}；{6}≠O，因為 6∉O；{6}≠E，因為 2∈E 但 2∉{6}；{6}≠S，因為 1∈S 但 1∉{6}。四個都不相等，所以 {6}∉F₀。



S12 · implies操作前

\{6\}\subseteq S,\ |S|=6,\ \{6\}\notin F_0

操作後

\{6\}\ \text{is not an event of}\ (S,F_0)

條件：F_0\ \text{an event family}

規則：mko_event_def · 依賴：S10, S11

葉節點依據：mko_event_def + powerset_def

依 MKO，一般模型 (S,F) 中事件必須屬於 F。{6}⊆S，S 也只有 6 個元素，但 {6}∉F₀（S11），所以在 M2 中 {6} 不是事件；「擲出 6」不能在 M2 中當作事件討論。S 有限並不會讓每個子集合自動成為事件；在 M1 中 {6} 是事件，只因為 M1 明示採用 F=𝒫(S)。



S13 · implies操作前

E\in F_0,\ \omega=4

操作後

E\ \text{is an event of}\ (S,F_0)\ \text{and occurs}

條件：無

規則：mko_event_def · 依賴：S04, S10

葉節點依據：mko_event_def

E 是 F₀ 的成員，所以在 M2 中 E 也是事件；觀察到 ω=4 時 4∈E，E 發生。同一個集合 E 在兩個模型中都是事件，而 {6} 只在 M1 中是事件：是否為事件取決於事件族，不只取決於 S。



S14 · implies操作前

\text{models}\ (S,\mathcal{P}(S))\ \text{and}\ (S,F_0)

操作後

E\ \text{event in both};\ \{6\}\ \text{event in}\ (S,\mathcal{P}(S))\ \text{only}

條件：無

規則：and_intro_elim · 依賴：S03, S04, S05, S06, S10, S12, S13

葉節點依據：and_intro_elim

彙整：在 M1 中 E 是事件，ω=4 時發生、ω=3 時不發生（S03、S04）；結果 4 不同於事件 {4}（S05）；∅ 從不發生，S 總是發生（S06）。在 M2 中 F₀ 是事件族（S10），E 仍是事件（S13），但 {6} 不是（S12）。







## 局部子步與引理

S10.1 · implies操作前

X\in F_0

操作後

X=\bigcup\{A\in\{E,O\}\mid A\subseteq X\}

條件：無

規則：set_extensionality · 依賴：S09

葉節點依據：set_extensionality + subset_def + set_operations_def

對 F₀ 的四個成員逐一核對：沒有原子包含於 ∅（E、O 都非空），空族的聯集是 ∅；包含於 E 的原子只有 E（1∈O 但 1∉E），聯集是 E；同理，包含於 O 的只有 O；包含於 S 的原子是 E 與 O，聯集 E∪O=S（S09）。所以每個 X∈F₀ 都等於它所包含的原子之聯集。



S10.2 · equivalent操作前

x\in\bigcup_{i}X_i

操作後

x\in\bigcup\{A\in\{E,O\}\mid\exists i,\ A\subseteq X_i\}

條件：X_i\in F_0\ \text{for all}\ i

規則：set_operations_def · 依賴：S10.1

葉節點依據：set_operations_def + eq_replace + exists_intro + exists_elim

x 屬於聯集 ⇔ 有某個 i 使 x∈X_i ⇔（依 S10.1）有某個 i 與某個原子 A⊆X_i 使 x∈A ⇔ x 屬於某個「包含於某個 X_i 的原子」。交換兩個存在量詞的次序不改變真假。所以可數聯集等於這些原子的聯集。



S10.3 · implies操作前

\{A\in\{E,O\}\mid\exists i,\ A\subseteq X_i\}

操作後

\bigcup_i X_i\in\{\varnothing,E,O,S\}=F_0

條件：無

規則：case_analysis · 依賴：S10.2, S09

葉節點依據：case_analysis + set_operations_def

被選出的原子族是 {E,O} 的子族，只有四種可能：空族、{E}、{O}、{E,O}，對應的聯集分別是 ∅、E、O、E∪O=S，全都屬於 F₀。S10.1 到 S10.3 合起來證得引理 L_F0_unions。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S03, S04, S05, S06, S10, S12, S13, and_intro_elim — 目標 G 是題目各項結論的合取；每一項由所列步驟正向證成，此步只做合取，沒有把 G 當作前提。
- S13 · premise_audit · mko_event_def, S10 — 需要 E∈F₀（G3 的列舉）與 F₀ 合法（S10）；發生與否的判定與 S04 相同。
- S12 · premise_audit · mko_event_def, S10, S11 — 需要 F₀ 是合法事件族（S10），否則 M2 不是模型，結論沒有意義。
- S11 · premise_audit · set_extensionality, G3 — F₀ 是有限列舉，與每個成員比較就是完整檢查；每個不等都有一個見證元素。
- S10.3 · premise_audit · S10.2, S09, case_analysis — 四種情況窮盡 {E,O} 的子族；論證對任意可數族成立，與族中列出多少個集合無關。
- S10.2 · inverse_equivalence · S10.1, set_operations_def, exists_intro, exists_elim — 每一步都是等價：聯集的定義、S10.1 的集合相等、存在量詞的交換；所以兩邊元素相同。
- S10.1 · premise_audit · S09, set_extensionality, subset_def — F₀ 的四個成員全部檢查，是完整窮舉；這個性質只對 F₀ 的成員宣稱。
- S10 · premise_audit · S07, S08, L_F0_unions, sigma_algebra_def — 三條各由一步提供；不宣稱 F₀ 包含 S 的所有子集合（S11 正好相反）。
- S09 · premise_audit · set_operations_def, set_extensionality — 對 S 的六個元素逐一檢查，是完整窮舉。
- S08 · premise_audit · set_operations_def, set_extensionality, sigma_algebra_def — F₀ 只有四個成員，逐一計算就是完整檢查。
- S07 · premise_audit · sigma_algebra_def, S02 — 只核對第一條；其餘兩條在 S08、S10。
- S06 · premise_audit · powerset_def, subset_def, mko_event_def, G1 — S 總是發生需要樣本空間的完整性（G1）；不宣稱 P(∅)=0 或 P(S)=1，那需要另給機率模型。
- S05 · premise_audit · powerset_def, subset_def, mko_event_def — {4}⊆S 因為它唯一的元素 4 在 S 中；{4}∈F 依賴 M1 的 F=𝒫(S)，在 M2 中不一定成立（S11 處理同類的 {6}）。
- S04 · premise_audit · mko_event_def, S03 — 需要 E 已是事件（S03）；「發生」只對事件定義。這裡不宣稱任何機率值。
- S03 · inverse_equivalence · powerset_def, G2 — 冪集定義是雙向的；但這個等價只在 F=𝒫(S) 的模型中把子集合與事件連起來。
- S02 · premise_audit · subset_def — 完整窮舉，不是抽樣；反向 S⊆E 不宣稱（1∉E）。
- S01 · premise_audit · G1, G2, G3, def_intro — 此步只寫出資料並命名，不推出新事實；S 與兩個事件族都已明示，符合假設 a1、a2。





## 錯誤控制與反例

事件不是單一結果MKO 指出常見誤解是把事件當成單一結果。4 是 S 的元素（結果），{4} 是 S 的子集合（事件），4≠{4}；而 E={2,4,6} 含三個結果（S05）。說「E 發生」是說觀察到的結果屬於 E，不是說觀察到的結果等於 E。

先指定樣本空間與事件族MKO 提醒不要在未指定樣本空間或事件族時列事件。問「{6} 是不是事件」沒有固定答案：在 M1 中是，在 M2 中不是（S12）。所以每次列事件之前，都要說明 S 與 F。

S 有限不代表所有子集合都是事件MKO 指出另一個誤解：樣本空間有限就自動讓所有子集合可測。M2 的 S 只有 6 個元素，F₀ 是合法事件族（S07、S08、S10），但 {6}∉F₀。只有明示採 F=𝒫(S) 時，每個子集合才是事件。


- S 有限，所以在任何模型 (S,F) 中 {6} 都是事件 → reject — 在 M2 中 {6}∉F₀（S11、S12）。
- 事件 E={2,4,6} 就是結果 4 → reject — E 是含三個結果的集合；4 只是其中一個元素（S05）。
- 觀察到 3 時，事件 E={2,4,6} 發生 → reject — 3∉E，所以 E 不發生（S04）。
- E 是事件，所以 P(E)=1/2 → reject — 本稿兩個模型都沒有指派機率；是否為事件不決定機率值。
- F₀ 不含 {6}，所以 F₀ 不是事件族 → reject — σ-代數的三條在 S07、S08、S10 都已核對；事件族不必包含單點集合。





## 結論與限制

在有限初等模型 F=𝒫(S) 中，E={2,4,6} 是事件；觀察到 4 時 E 發生，觀察到 3 時不發生；結果 4 與事件 {4} 不同；空事件從不發生，必然事件總是發生。在一般模型 (S,F₀) 中，F₀={∅,{1,3,5},{2,4,6},S} 是事件族，E 仍是事件，但 {6}∉F₀，所以雖然 S 有限且 {6}⊆S，{6} 不是事件。


- 一般模型的事件族採用標準的 σ-代數定義（sigma_algebra_def）作為前置知識；MKO 本身只要求事件屬於明示的 F。
- N1、N2 以餘數核對 4 為偶數、3 為奇數，只是交叉核對；論證依據的是 E 與 O 的列舉。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 5f67b035b93e0779d5d9d9a91ef38849d1d4aa6bcd00b2c987bd6528a63147cd
- original source SHA-256: 5f67b035b93e0779d5d9d9a91ef38849d1d4aa6bcd00b2c987bd6528a63147cd
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-event-01.json)