# 事件獨立：以交集乘積判定，並核對條件式、補集與零機率事件

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

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

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



## 目標與範圍

公正骰子模型：Ω={1,2,3,4,5,6}，每個結果的質量為 1/6。設 A={2,4,6}、B={1,2,3,4}、D={1,3,5}、Z=∅。（一）以乘積定義判定 A 與 B 是否獨立，並在 P(B)>0 下核對 P(A|B)=P(A)。（二）證明 A 與 B 獨立推出 A 與 Bᶜ 獨立，並以數字核對。（三）判定互斥事件 A、D 是否獨立。（四）判定 A 與零機率事件 Z 是否獨立，並說明條件式為何不能使用。

在 MKO 的範圍內工作：樣本空間、精確有理質量與事件子集完整明示（假設 a1）；只處理兩個事件的獨立（假設 a2），三事件的例子只出現在錯誤控制與負向控制中，用來說明兩兩獨立不能冒充相互獨立。不處理無限樣本空間或隨機變數的獨立（後者屬下一節點），不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- prob_axioms
- set_operations_def
- frac_rules
- mul_inverse_nonzero
- numeric_evaluation


- G1 — Ω={1,2,3,4,5,6}，事件族為 Ω 的全部子集，每個結果的質量 m(ω)=1/6，P(E)=Σ_{ω∈E} m(ω)。
- G2 — A={2,4,6}、B={1,2,3,4}、D={1,3,5}、Z=∅，四者都是同一個 Ω 的子集。


- \Omega=\{1,2,3,4,5,6\} — 樣本空間
- m(\omega)=\tfrac16 — 每個結果的質量
- P(E) — 事件 E 的機率，E 中質量之和
- A,B,D,Z — 四個給定事件；Z=∅
- B^c — B 在 Ω 中的補集
- P(A\mid B) — 條件機率，只在 P(B)>0 時有定義





## 規則與來源


- prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
- 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。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- 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。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_event_indep_def · cited — 在同一機率空間中，A 與 B 獨立當且僅當 P(A∩B)=P(A)P(B)。若 P(B)>0，這等價於 P(A|B)=P(A)；P(B)=0 時不得以未定義的條件機率取代乘積定義。 · mko-event-independence
- cond_prob_def · cited — 在有限樣本空間中，對 P(B)>0 定義 P(A|B)=P(A∩B)/P(B)；若 P(B)=0，這個條件機率不定義，即使 B 非空。 · mko-conditional-probability
- point_mass_sum · prerequisite — 有限模型中事件的機率是其中各結果質量之和：P(E)=Σ_{ω∈E} m(ω)；空和為 0。
- L_cond_equiv · lemma — 若 P(B)>0，則 P(A∩B)=P(A)P(B) ⇔ P(A|B)=P(A)。
- L_complement · lemma — 在同一機率空間中，若 P(A∩B)=P(A)P(B)，則 P(A∩Bᶜ)=P(A)P(Bᶜ)。





## 逐步主鏈

S01 · definition操作前

\Omega=\{1,2,3,4,5,6\},\ m(\omega)=\tfrac16

操作後

P(E)=\sum_{\omega\in E}m(\omega)=\tfrac{|E|}{6},\ \ P(\Omega)=6\cdot\tfrac16=1

條件：無

規則：point_mass_sum · 依賴：G1

葉節點依據：point_mass_sum + prob_axioms + numeric_evaluation

所有事件都在同一個模型中計算機率：P(E) 是 E 中質量之和；因每個質量都是 1/6，P(E)=|E|/6。總質量 6·(1/6)=1，所以這是歸一化的機率模型。MKO 要求兩個事件屬於同一機率空間，這一步把它固定下來。



S02 · equivalent操作前

P(A),\ A=\{2,4,6\}

操作後

P(A)=\tfrac36=\tfrac12

條件：無

規則：point_mass_sum · 依賴：S01, G2

葉節點依據：point_mass_sum + frac_rules + numeric_evaluation

A 有 3 個結果，P(A)=3·(1/6)=3/6=1/2。



S03 · equivalent操作前

P(B),\ B=\{1,2,3,4\}

操作後

P(B)=\tfrac46=\tfrac23

條件：無

規則：point_mass_sum · 依賴：S01, G2

葉節點依據：point_mass_sum + frac_rules + numeric_evaluation

B 有 4 個結果，P(B)=4/6=2/3（分子分母同除 2）。



S04 · equivalent操作前

A\cap B

操作後

\{2,4\}

條件：無

規則：set_operations_def · 依賴：G2

葉節點依據：set_operations_def + set_extensionality

交集由同時屬於 A 與 B 的結果組成：2、4 屬於兩者；6 不在 B；1、3 不在 A；5 兩者都不在。



S05 · equivalent操作前

P(A\cap B)=P(\{2,4\})

操作後

P(A\cap B)=\tfrac26=\tfrac13

條件：無

規則：point_mass_sum · 依賴：S01, S04

葉節點依據：point_mass_sum + frac_rules + numeric_evaluation

A∩B 有 2 個結果，機率 2/6=1/3。



S06 · equivalent操作前

P(A)P(B)

操作後

\tfrac12\cdot\tfrac23=\tfrac13

條件：無

規則：frac_rules · 依賴：S02, S03

葉節點依據：frac_rules + numeric_evaluation

分數相乘：(1/2)(2/3)=2/6=1/3。



S07 · equivalent操作前

P(A\cap B)=\tfrac13=P(A)P(B)

操作後

A,\ B\ \text{independent}

條件：無

規則：mko_event_indep_def · 依賴：S05, S06, mko_event_indep_def

葉節點依據：mko_event_indep_def + def_unfold + eq_refl_symm_trans

依 MKO 的主資格，獨立就是交集機率等於兩個機率的乘積。S05 與 S06 給出兩邊都是 1/3，所以 A 與 B 獨立。判定用的是精確有理數相等，不是近似。



S08 · implies操作前

P(B)=\tfrac23>0

操作後

P(A\mid B)=\frac{P(A\cap B)}{P(B)}=\frac{1/3}{2/3}=\tfrac12

條件：P(B)>0

規則：cond_prob_def · 依賴：S03, S05, cond_prob_def

葉節點依據：cond_prob_def + frac_rules + numeric_evaluation

因 P(B)=2/3>0，條件機率有定義：P(A|B)=(1/3)/(2/3)=(1/3)(3/2)=1/2。直觀上，已知結果在 {1,2,3,4} 中時，偶數 2、4 佔一半。



S09 · implies操作前

P(A\mid B)=\tfrac12,\ P(A)=\tfrac12,\ P(B)>0

操作後

P(A\mid B)=P(A),\ \text{consistent with}\ P(A\cap B)=P(A)P(B)

條件：P(B)>0

規則：L_cond_equiv · 依賴：S02, S07, S08

葉節點依據：L_cond_equiv + eq_refl_symm_trans

S08 給 P(A|B)=1/2=P(A)。依引理 L_cond_equiv（在 P(B)>0 下乘積式與條件式等價），這與 S07 的乘積判定一致：知道 B 發生不改變 A 的機率。引理在子步 S09.1、S09.2 證明。



S10 · implies操作前

P(A\cap B)=P(A)P(B)

操作後

P(A\cap B^c)=P(A)P(B^c)

條件：無

規則：L_complement · 依賴：S07

葉節點依據：prob_axioms + distributive

MKO 指出事件與補集的獨立可由同一等式推導。依引理 L_complement，由 S07 得 A 與 Bᶜ 也獨立。引理在子步 S10.1 到 S10.3 證明，只用可加性與分配律，不需要 P(B)>0。



S11 · implies操作前

B^c=\{5,6\},\ A\cap B^c=\{6\}

操作後

P(A\cap B^c)=\tfrac16=\tfrac12\cdot\tfrac13=P(A)P(B^c)

條件：無

規則：numeric_evaluation · 依賴：S01, S02, S03, S10

葉節點依據：numeric_evaluation + set_operations_def + frac_rules

直接核對：Bᶜ={5,6}，P(Bᶜ)=1/3；A∩Bᶜ={6}，機率 1/6；乘積 (1/2)(1/3)=1/6。與 S10 的一般推論一致，也與 S10.2 的 P(A)−P(A∩B)=1/2−1/3=1/6 一致。



S12 · implies操作前

A\cap D=\{2,4,6\}\cap\{1,3,5\}=\varnothing

操作後

P(A\cap D)=0\neq\tfrac14=P(A)P(D)\ \Rightarrow\ A,D\ \text{not independent}

條件：無

規則：mko_event_indep_def · 依賴：S01, S02, G2, mko_event_indep_def

葉節點依據：mko_event_indep_def + point_mass_sum + numeric_evaluation

A 與 D 互斥：沒有結果同時是偶數與奇數，P(A∩D)=P(∅)=0。但 P(D)=3/6=1/2，P(A)P(D)=1/4≠0。乘積等式不成立，所以 A 與 D 不獨立。互斥反而表示強烈相依：知道 D 發生就知道 A 不發生。



S13 · implies操作前

A\cap D=\varnothing,\ P(A)>0,\ P(D)>0

操作後

P(A\cap D)=0<P(A)P(D)\ \Rightarrow\ A,D\ \text{not independent}

條件：P(A)>0; P(D)>0

規則：order_basics · 依賴：S12, mko_event_indep_def

葉節點依據：order_basics + prob_axioms + mko_event_indep_def

一般化：任何兩個互斥且機率皆為正的事件都不獨立，因為兩個正數的乘積為正，而交集機率為 0。條件「機率皆為正」不可省略：若其中一個機率為 0，見 S14。



S14 · implies操作前

Z=\varnothing,\ P(Z)=0

操作後

P(A\cap Z)=0=P(A)\cdot 0=P(A)P(Z)\ \Rightarrow\ A,Z\ \text{independent};\ P(A\mid Z)\ \text{undefined}

條件：無

規則：mko_event_indep_def · 依賴：S01, S02, G2, mko_event_indep_def, cond_prob_def

葉節點依據：mko_event_indep_def + mul_zero + prob_axioms

在本模型中，每個非空事件至少有質量 1/6，所以唯一的零機率事件是 Z=∅。A∩Z=∅，P(A∩Z)=0，而 P(A)P(Z)=(1/2)·0=0，乘積等式成立，所以依定義 A 與 Z 獨立。另一方面 P(Z)=0，P(A|Z) 依條件機率定義不存在；MKO 規定此時不得以未定義的條件機率代替乘積定義。



S15 · implies操作前

\text{S07},\ \text{S09},\ \text{S10},\ \text{S12},\ \text{S14}

操作後

A\perp B;\ A\perp B^c;\ A\not\perp D;\ A\perp Z

條件：無

規則：and_intro_elim · 依賴：S07, S09, S10, S11, S12, S14

葉節點依據：and_intro_elim

合併四個任務：A 與 B 獨立（乘積式，並以條件式核對）；A 與 Bᶜ 獨立（一般引理加數字核對）；互斥的 A、D 不獨立；A 與零機率事件 Z 依乘積定義獨立，而 P(A|Z) 無定義。







## 局部子步與引理

S09.1 · equivalent操作前

P(A\mid B)=P(A)

操作後

\frac{P(A\cap B)}{P(B)}=P(A)

條件：P(B)>0

規則：cond_prob_def · 依賴：cond_prob_def

葉節點依據：cond_prob_def + def_unfold

在 P(B)>0 下，依條件機率定義把 P(A|B) 換成 P(A∩B)/P(B)。若 P(B)=0，左式根本沒有定義，這一步不能做。



S09.2 · equivalent操作前

\frac{P(A\cap B)}{P(B)}=P(A)

操作後

P(A\cap B)=P(A)P(B)

條件：P(B)\neq 0

規則：mul_inverse_nonzero · 依賴：S09.1, mul_inverse_nonzero

葉節點依據：eq_congruence + mul_inverse_nonzero + mul_assoc + mul_one

兩邊同乘 P(B)；反向是兩邊同乘 1/P(B)，需要 P(B)≠0，由 P(B)>0 保證。S09.1 與 S09.2 合起來證得引理 L_cond_equiv。



S10.1 · equivalent操作前

A

操作後

A=(A\cap B)\cup(A\cap B^c),\ \ (A\cap B)\cap(A\cap B^c)=\varnothing

條件：無

規則：set_operations_def · 依賴：set_operations_def

葉節點依據：set_operations_def + set_extensionality

A 的每個結果要嘛在 B 中、要嘛在 Bᶜ 中，恰好一種，所以 A 是 A∩B 與 A∩Bᶜ 的不交聯集。



S10.2 · implies操作前

A=(A\cap B)\sqcup(A\cap B^c)

操作後

P(A)=P(A\cap B)+P(A\cap B^c)

條件：無

規則：prob_axioms · 依賴：S10.1, prob_axioms

葉節點依據：prob_axioms + eq_congruence

不交事件的機率相加（機率公理），所以 P(A) 等於兩部分之和；移項得 P(A∩Bᶜ)=P(A)−P(A∩B)。



S10.3 · implies操作前

P(A\cap B^c)=P(A)-P(A\cap B)

操作後

P(A\cap B^c)=P(A)-P(A)P(B)=P(A)(1-P(B))=P(A)P(B^c)

條件：P(A\cap B)=P(A)P(B)

規則：distributive · 依賴：S10.2, prob_axioms, distributive

葉節點依據：distributive + prob_axioms + eq_replace

代入假設 P(A∩B)=P(A)P(B)，提出公因子 P(A)，再用 P(Bᶜ)=1−P(B)（機率公理的推論）。S10.1 到 S10.3 合起來證得引理 L_complement。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S07, S10, S12, S14, and_intro_elim — 目標 G 是四個判定的合取；足夠條件 H 是 S07、S10、S12、S14，H⇒G 由合取引入，H 由已知正向證得，沒有把 G 當作前提。
- S14 · premise_audit · mko_event_indep_def, cond_prob_def, mul_zero — 判定只用乘積定義與 u·0=0（N10）；沒有使用 P(A|Z)，也不宣稱它等於任何數。
- S13 · premise_audit · order_basics, prob_axioms — 需要 u>0、w>0 ⇒ uw>0（順序公理）與 P(∅)=0；不宣稱反向，即不宣稱不獨立的事件必互斥。
- S12 · premise_audit · mko_event_indep_def, S02, numeric_evaluation — 否定獨立只需乘積等式在這一對事件不成立（N9）。
- S11 · premise_audit · S01, S10, numeric_evaluation — 這是對這組數字的獨立重算（N7、N8），不是 L_complement 的證明。
- S10.3 · premise_audit · S10.2, distributive, prob_axioms — 用到的假設只有乘積等式本身；推導中沒有除法，所以不需要 P(B)>0 或 P(A)>0。
- S10.2 · premise_audit · S10.1, prob_axioms — 可加性需要兩部分不交，S10.1 已確認；若兩部分重疊，和會重複計算。
- S10.1 · inverse_equivalence · set_operations_def, set_extensionality — x∈A ⇔ x∈A∩B 或 x∈A∩Bᶜ，兩邊元素相同；不交性來自 B∩Bᶜ=∅。
- S10 · premise_audit · S07, L_complement — 需要 S07 的乘積等式；反向（由 A⊥Bᶜ 推回 A⊥B）也成立，因為 (Bᶜ)ᶜ=B，但本步不使用。
- S09.2 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — 乘 P(B) 與乘 1/P(B) 互為反運算，條件 P(B)≠0。
- S09.1 · inverse_equivalence · cond_prob_def, def_unfold — 展開與折回定義互為反操作，前提 P(B)>0。
- S09 · premise_audit · S08, L_cond_equiv — 引理需要 P(B)>0，S03 已確認。主資格仍是 S07 的乘積式；條件式只是在正分母時的等價核對。
- S08 · premise_audit · S03, S05, cond_prob_def, frac_rules — 前提是 P(B)>0；沒有它，這個除法不被允許（見 S14）。數值由 N6 核對。
- S07 · inverse_equivalence · mko_event_indep_def, S05, S06 — MKO 的定義是「當且僅當」，所以這一步雙向成立：獨立也推回乘積等式。
- S06 · inverse_equivalence · frac_rules, numeric_evaluation — 精確有理數運算，兩邊同值（N5），雙向成立。
- S05 · inverse_equivalence · point_mass_sum, frac_rules — 同 S03，約分雙向成立（N4）。
- S04 · inverse_equivalence · set_operations_def, set_extensionality — 逐一核對 Ω 的六個結果，兩邊含有相同元素，依集合外延性相等。
- S03 · inverse_equivalence · point_mass_sum, frac_rules — 約分是等值改寫，2/3=4/6，雙向成立（N3）。
- S02 · inverse_equivalence · point_mass_sum, numeric_evaluation — 反向：1/2=3/6 是 A 的三個質量之和，兩式表示同一個數（N2）。
- S01 · premise_audit · G1, point_mass_sum — 只寫出模型並核對總和為 1（N1）；之後所有機率都由這個 P 計算，不能混用另一個模型的數字。





## 錯誤控制與反例

互斥不代表獨立MKO 指出的第一個誤解是把互斥當獨立。互斥是集合關係 A∩D=∅；獨立是機率關係 P(A∩D)=P(A)P(D)。S12、S13 顯示：兩個機率為正的互斥事件必不獨立，因為 0<P(A)P(D)。

P(B)=0 時用乘積定義條件式 P(A|B)=P(A) 只在 P(B)>0 時與獨立等價（S09）。P(B)=0 時 P(A|B) 無定義，不能「算出來」再比較，也不能自行定義為 P(A)。乘積定義仍然可用，並給出：零機率事件與每個事件都獨立（S14）。

兩兩獨立不保證相互獨立本稿只處理兩個事件。對三個事件，兩兩獨立不能推出相互獨立：擲兩枚公正硬幣，Ω′={HH,HT,TH,TT}，E₁=第一枚正面、E₂=第二枚正面、E₃=兩枚相同。每兩個的交集都是 {HH}，機率 1/4=(1/2)(1/2)；但 P(E₁∩E₂∩E₃)=1/4≠1/8=(1/2)³。


- A={2,4,6} 與 D={1,3,5} 沒有共同結果，所以兩者獨立 → reject — P(A∩D)=0，但 P(A)P(D)=1/4；乘積等式不成立。
- P(A|∅) 無定義，所以無法判定 A 與 ∅ 是否獨立 → reject — 主資格是乘積定義：P(A∩∅)=0=P(A)·0，所以 A 與 ∅ 獨立。
- P(B)=0 時可以約定 P(A|B)=P(A)，再用條件式判定獨立 → reject — MKO 明文禁止以未定義的條件機率取代乘積定義；P(B)=0 時只能用 P(A∩B)=P(A)P(B)。
- 兩枚硬幣例子中 E₁、E₂、E₃ 兩兩獨立，所以三者相互獨立 → reject — P(E₁∩E₂∩E₃)=1/4，而 P(E₁)P(E₂)P(E₃)=1/8。





## 結論與限制

在公正骰子模型中，P(A∩B)=1/3=P(A)P(B)，所以 A={2,4,6} 與 B={1,2,3,4} 獨立，且因 P(B)>0，P(A|B)=1/2=P(A)。由同一等式推出 A 與 Bᶜ 獨立，數字核對 1/6=(1/2)(1/3)。互斥的 A 與 D={1,3,5} 不獨立（0≠1/4）。A 與零機率事件 ∅ 依乘積定義獨立，而條件機率 P(A|∅) 無定義、不得使用。


- 三事件的相互獨立只在錯誤控制中以反例說明，沒有完整的定義與定理；這屬於 MKO 範圍之外。
- N11、N12 屬於兩枚硬幣模型 Ω′，與骰子模型 Ω 分開；兩者的數字不可混用。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 95a388554abac792bff1076b0a008b4da36c317d8313513927b13a553a4460d7
- original source SHA-256: 95a388554abac792bff1076b0a008b4da36c317d8313513927b13a553a4460d7
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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