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

目標與範圍

公正骰子模型：Ω={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ᶜ)。

逐步主鏈

\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

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

P(A)=\tfrac36=\tfrac12

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

P(B)=\tfrac46=\tfrac23

A\cap B

\{2,4\}

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

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

P(A)P(B)

\tfrac12\cdot\tfrac23=\tfrac13

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

A,\ B\ \text{independent}

P(B)=\tfrac23>0

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

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(A\cap B)=P(A)P(B)

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

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

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

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}

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}

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}

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

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

局部子步與引理

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

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

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

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

A

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

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

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

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)

逐步反向審查

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