有限模型的條件機率：正分母、兩個方向與零機率條件

目標與範圍

在 S={1,2,3,4,5,6}、權重 w=(1,2,3,2,4,0)/12 的有限模型中，設 A={2,3}、B={3,4,5,6}、Z={6}。驗證模型合法，計算 P(A|B) 與 P(B|A)，與等可能計數比 |A∩B|/|B| 及乘積 P(A)P(B) 比較，並判定 P(A|Z) 是否有定義。

在 MKO 的範圍內工作：非空有限樣本空間、全冪集事件族、已歸一化的非負有理權重。只在 P(B)>0 時定義 P(A|B)=P(A∩B)/P(B)，並證明一個加法小引理（E⊆E′ 時 P(E′)=P(E)+P(E′∖E)）以說明 0≤P(A|B)≤1。不定義零機率條件化；不討論事件獨立性、貝氏定理或無限樣本空間；不改動 canonical MKO 或英文 edition。

已知條件與符號

• prob_axioms
• set_operations_def
• subset_def
• frac_rules
• numeric_evaluation
• weight_model

• G1 — S={1,2,3,4,5,6}，事件族 F=𝒫(S)，權重 w(1)=1/12、w(2)=2/12、w(3)=3/12、w(4)=2/12、w(5)=4/12、w(6)=0；P(E)=Σ_{s∈E} w(s)。此模型未宣告為等可能。
• G2 — 事件 A={2,3}、B={3,4,5,6}、Z={6}。
• G3 — 待辦：驗證模型與事件資格；求 P(A|B)、P(B|A)；比較 |A∩B|/|B| 與 P(A)P(B)；判定 P(A|Z)。

• S — 樣本空間 {1,2,3,4,5,6}
• w(s) — 樣本點 s 的權重
• P(E) — 事件 E 的機率 Σ_{s∈E} w(s)
• P(A\mid B) — 在 B 之下 A 的條件機率，即 C(A,B)
• A^{c} — S∖A

規則與來源

• 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。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• 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）。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
• 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。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_cond_prob_def · cited — 在非空有限樣本空間 S、全冪集事件族 F=𝒫(S) 與已歸一化非負有理權重下，對 A、B⊆S 且 P(B)>0，定義 C(A,B)=P(A|B)=P(A∩B)/P(B)。若 P(B)=0，本條目不定義這個條件機率，即使 B 非空。 · mko-conditional-probability
• weight_model · prerequisite — 有限權重模型：w:S→ℚ，對每個 s 有 w(s)≥0，且 Σ_{s∈S} w(s)=1；事件 E⊆S 的機率是 P(E)=Σ_{s∈E} w(s)（空和為 0）。
• L_split · lemma — 在有限權重模型中，若 E⊆E′⊆S，則 P(E′)=P(E)+P(E′∖E)，因此 P(E)≤P(E′)。

逐步主鏈

w=\left(\tfrac{1}{12},\tfrac{2}{12},\tfrac{3}{12},\tfrac{2}{12},\tfrac{4}{12},0\right)

w(s)\ge 0,\quad \sum_{s\in S}w(s)=\tfrac{12}{12}=1

A=\{2,3\},\ B=\{3,4,5,6\},\ Z=\{6\}

A,B,Z\subseteq S

P(B)=w(3)+w(4)+w(5)+w(6)

P(B)=\tfrac{3+2+4+0}{12}=\tfrac{9}{12}=\tfrac{3}{4}

P(B)=\tfrac{3}{4}

P(B)>0,\ \text{so}\ P(A\mid B)\ \text{is defined}

A\cap B

\{3\}

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

w(3)=\tfrac{3}{12}=\tfrac{1}{4}

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

\frac{1/4}{3/4}=\frac{1}{3}

\frac{3/12}{9/12}

\frac{3}{9}=\frac{1}{3}

A\cap B\subseteq B

P(A\cap B)\le P(B),\ \text{so}\ 0\le P(A\mid B)\le 1

B\setminus(A\cap B)=A^{c}\cap B=\{4,5,6\}

P(A^{c}\cap B)=\tfrac{1}{2},\ P(A\mid B)+P(A^{c}\mid B)=\tfrac{1}{3}+\tfrac{2}{3}=1

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

P(A)=\tfrac{5}{12}>0,\quad P(B\mid A)=\frac{1/4}{5/12}=\frac{3}{5}\neq\frac{1}{3}

\frac{|A\cap B|}{|B|}=\frac{1}{4}

\frac{1}{4}\neq\frac{1}{3}=P(A\mid B)

P(A)P(B)=\tfrac{5}{12}\cdot\tfrac{3}{4}

\tfrac{5}{16}\neq\tfrac{1}{3}=P(A\mid B)

Z=\{6\}\neq\varnothing,\ P(Z)=w(6)

P(Z)=0,\ \text{so}\ P(A\mid Z)\ \text{is undefined}

\text{S01 to S14}

P(A\mid B)=\tfrac{1}{3},\ P(B\mid A)=\tfrac{3}{5},\ P(A\mid Z)\ \text{undefined}

局部子步與引理

E\subseteq E'\subseteq S

P(E')=P(E)+P(E'\setminus E)\ge P(E)

逐步反向審查

• S15 · sufficient_goal_reduction · S01, S07, S11, S12, S13, S14, and_intro_elim — 目標 G：題目各項。足夠條件 H：所列各步的結論；H⇒G 只是合取，H 由 G1、G2 正向證成，沒有把 G 當作前提。
• S14 · premise_audit · mko_cond_prob_def, mul_inverse_nonzero — 判定只依 P(Z)=0；非空不足以條件化。不宣稱其他理論中零機率條件化的處理。
• S13 · premise_audit · frac_rules, numeric_evaluation — 只需精確比較兩個有理數；本稿不由此推論任何獨立性結論。
• S12 · premise_audit · mko_cond_prob_def, weight_model — 只需一組不相等的權重就說明模型不是等可能；此步只排除錯誤算法。
• S11 · premise_audit · mko_cond_prob_def, set_operations_def, frac_rules — 兩個方向各自需要正分母（MKO 第三段）；交集可交換，但分母不能互換。
• S10 · premise_audit · L_split, S03, S06, frac_rules — 這是獨立的一致性檢查，不是 P(A|B) 的推導所必需。
• S09.1 · premise_audit · weight_model, set_operations_def, finite_sum_rules, order_basics — 需要互斥拆分與權重非負；若允許負權重，不等式部分就不成立。
• S09 · premise_audit · L_split, order_basics — 除以正數保持不等式方向，所以需要 P(B)>0；引理在 S09.1 證明。
• S08 · inverse_equivalence · frac_rules — 分數規則在分母非零時是等式，雙向成立。
• S07 · inverse_equivalence · frac_rules, mul_inverse_nonzero — 反向：P(A|B)·P(B)=(1/3)·(3/4)=1/4=P(A∩B)（N5）；乘以 3/4 與除以 3/4 互為反運算，前提是 3/4≠0。
• S06 · inverse_equivalence · weight_model, frac_rules — 精確求值，兩向成立。
• S05 · inverse_equivalence · set_operations_def, set_extensionality — 兩個集合有相同元素，依集合相等兩向成立。
• S04 · premise_audit · mko_cond_prob_def, order_basics — 需要的是 P(B) 嚴格大於零，不是 B 非空（見 S14）。
• S03 · inverse_equivalence · weight_model, frac_rules, numeric_evaluation — 有理數的精確求值，兩邊是同一個數。
• S02 · premise_audit · subset_def — 逐元素核對即可；不宣稱反向。
• S01 · premise_audit · weight_model, numeric_evaluation — 兩個條件（非負、總和 1）都必須核對；之後所有機率都依賴這一步。

錯誤控制與反例

非空不等於正機率

MKO 指出的第一個誤解是把非空當正機率。Z={6} 非空，但 w(6)=0，所以 P(Z)=0，不能在 Z 上條件化（S14）。條件化前要檢查的是 P(B)>0（S04），不是 B≠∅。

零機率條件不給零答案

MKO 的第二個誤解是對零機率條件給零答案。P(A|Z) 的式子分母為 0，0 沒有倒數，所以本條目中 P(A|Z) 沒有定義；寫成 0 或 1 都是錯的。

兩個方向不能混同

MKO 的第三個誤解是混同兩個方向。P(A|B)=1/3 以 P(B) 為分母，P(B|A)=3/5 以 P(A) 為分母（S07、S11），兩者不同，且各自都要先確認分母為正。同樣，條件機率不是 P(A)P(B)=5/16（S13），在非等可能模型中也不是計數比 1/4（S12）。

• Z={6} 非空，所以 P(A|Z) 有定義 → reject — P(Z)=w(6)=0；MKO 要求分母嚴格大於零。
• P(Z)=0，所以 P(A|Z)=0 → reject — 分母為 0 時式子沒有定義，不是 0。
• P(B|A)=P(A|B)=1/3 → reject — P(B|A)=(1/4)/(5/12)=3/5≠1/3。
• P(A|B)=|A∩B|/|B|=1/4 → reject — 模型不是等可能（w(5)=4/12、w(6)=0）；正確值 3/9=1/3。
• P(A|B)=P(A)P(B)=5/16 → reject — 條件機率是 P(A∩B)/P(B)=1/3，不是兩個機率的乘積。

結論與限制

權重 (1,2,3,2,4,0)/12 構成合法的有限模型。P(B)=3/4>0，P(A∩B)=1/4，所以 P(A|B)=1/3；P(A)=5/12>0，所以 P(B|A)=3/5，兩個方向不同。等可能計數比 1/4 與乘積 P(A)P(B)=5/16 都不是 P(A|B)。Z={6} 非空但 P(Z)=0，所以 P(A|Z) 在本條目中沒有定義。

• 本稿不討論事件獨立性；S13 只比較數值，不據此宣稱 A、B 是否獨立。
• 零機率條件化在其他理論（例如以極限或測度論的條件期望）中另有處理，不在本條目範圍。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 0c101f249b943132cf4ae7daef5fdcdd38e0b9d888feacc77fc0a88e0e9198d3
• original source SHA-256: 0c101f249b943132cf4ae7daef5fdcdd38e0b9d888feacc77fc0a88e0e9198d3
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）