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

目標與範圍

擲一顆骰子一次，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₀。

逐步主鏈

\text{one roll of a die}

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

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

E\subseteq S,\ O\subseteq S

E\subseteq S

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

\omega=4,\quad \omega=3

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

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

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

\varnothing\subseteq S,\ S\subseteq S

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

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

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

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

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

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

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

(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

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

\{6\}\notin F_0

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

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

E\in F_0,\ \omega=4

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

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

局部子步與引理

X\in F_0

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

x\in\bigcup_{i}X_i

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

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

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

逐步反向審查

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