# 有限樣本空間上的機率：驗證權重模型、計算事件機率與補事件

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

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

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



## 目標與範圍

S={1,2,3,4}，事件族為全冪集，權重 w_1=1/2、w_2=1/3、w_3=1/6、w_4=0。驗證這是合法的有限機率模型；由定義證明 P(∅)=0、P(S)=1、互斥可加與 P(S∖E)=1−P(E)；計算 P({1,3})，說明它不等於 |E|/|S|；說明 {4} 非空但機率為 0；並判定兩組候選權重 (1/2,1/3,1/3,0) 與 (1/2,2/3,−1/6,0) 都不合法。

在 MKO 的範圍內：非空有限樣本空間、全冪集事件族、精確有理權重（非負且總和恰為一），事件機率是成員權重之和。不推論真實實驗的機率，不處理獨立性、條件機率或一般測度論（MKO para2）；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- finite_sum_rules
- set_operations_def
- subset_def
- order_basics
- frac_rules
- numeric_evaluation


- G1 — S={1,2,3,4}，四個互異的結果標籤；事件族 F=𝒫(S)；權重 w_1=1/2、w_2=1/3、w_3=1/6、w_4=0（MKO 假設 a1、a2）。
- G2 — 要計算的事件：E={1,3}、Z={4}，以及 A={1,2}、C={2,3}。
- G3 — 比較用的候選權重：w′=(1/2,1/3,1/3,0) 與 w″=(1/2,2/3,−1/6,0)，依序對應結果 1、2、3、4。


- S — 樣本空間 {1,2,3,4}
- \mathcal{P}(S) — S 的全冪集（事件族）
- w_s — 結果 s 的有理權重
- P(E)=\sum_{s\in E}w_s — 事件 E 的機率
- S\setminus E — 相對於 S 的補事件
- |E| — 事件 E 的元素個數





## 規則與來源


- 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。
- 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)。
- 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。
- 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 — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_prob_def · cited — 令 S 為非空有限樣本空間，事件族 F=𝒫(S)。指定各 s∈S 的有理權重 w_s≥0 且 Σ_(s∈S)w_s=1，則事件 E⊆S 的機率 P(E)=Σ_(s∈E)w_s。只有另明示所有結果等可能，才可用 P(E)=|E|/|S|。 · mko-probability
- sum_split · prerequisite — 有限和的分割：對有限集合 S 上的數 w_s 與互斥子集合 A、C⊆S，Σ_{s∈A∪C} w_s=Σ_{s∈A} w_s+Σ_{s∈C} w_s；空集合上的和為 0。這是 finite_sum_rules 經重新編號所得。
- L_complement · lemma — 在合法的有限模型中，對每個事件 E⊆S，P(S∖E)=1−P(E)。
- L_equiprob · lemma — 若每個 w_s=1/|S|，則對每個 E⊆S，P(E)=|E|/|S|。





## 逐步主鏈

S01 · definition操作前

(S,\mathcal{P}(S),w)

操作後

P(E)=\sum_{s\in E}w_s\quad(E\subseteq S),\ \text{provided}\ w_s\geq 0,\ \sum_{s\in S}w_s=1

條件：S\ \text{finite, nonempty}

規則：mko_prob_def · 依賴：G1

葉節點依據：mko_prob_def + def_intro

依 MKO，有限機率模型由結果的權重決定：事件的機率是其成員權重之和。這個定義只有在權重合法（每個非負、總和恰為 1）時才給出機率律，所以必須先驗證權重（S03、S04），再計算任何事件。



S02 · implies操作前

E=\{1,3\},\ Z=\{4\},\ A=\{1,2\},\ C=\{2,3\}

操作後

E,Z,A,C\subseteq S,\ \text{hence}\ E,Z,A,C\in\mathcal{P}(S)

條件：無

規則：subset_def · 依賴：G1, G2, subset_def

葉節點依據：subset_def + set_builder

S 有限、非空，四個標籤互異。各事件的每個元素都在 S={1,2,3,4} 中，所以都是 S 的子集合；事件族是全冪集，因此它們都是事件（MKO 假設 a2：E 必須是 S 的子集合）。



S03 · implies操作前

w_1=\tfrac12,\ w_2=\tfrac13,\ w_3=\tfrac16,\ w_4=0

操作後

w_s\geq 0\ \text{for all}\ s\in S

條件：無

規則：order_basics · 依賴：G1, order_basics

葉節點依據：order_basics + numeric_evaluation

1/2、1/3、1/6 都是正有理數，w_4=0 也滿足 ≥0。四個結果逐一檢查，所以所有權重非負。



S04 · equivalent操作前

\sum_{s\in S}w_s=\tfrac12+\tfrac13+\tfrac16+0

操作後

\tfrac36+\tfrac26+\tfrac16+\tfrac06=\tfrac66=1

條件：無

規則：frac_rules · 依賴：G1, frac_rules

葉節點依據：frac_rules + numeric_evaluation

化為共分母 6：1/2=3/6、1/3=2/6、1/6=1/6、0=0/6，相加得 (3+2+1+0)/6=6/6=1。總和恰為 1，連同 S03，權重合法，P 是 S 上的機率律。



S05 · equivalent操作前

P(\varnothing)

操作後

\sum_{s\in\varnothing}w_s=0

條件：無

規則：sum_split · 依賴：S01, sum_split

葉節點依據：sum_split + finite_sum_rules

依定義 P(∅) 是空集合上的權重和，空和為 0，所以 P(∅)=0。



S06 · equivalent操作前

P(S)

操作後

\sum_{s\in S}w_s=1

條件：無

規則：def_unfold · 依賴：S01, S04

葉節點依據：def_unfold + eq_replace

依定義 P(S) 是全部權重之和，由 S04 等於 1。



S07 · implies操作前

A',C'\subseteq S,\ A'\cap C'=\varnothing

操作後

P(A'\cup C')=P(A')+P(C')

條件：A'\cap C'=\varnothing

規則：sum_split · 依賴：S01, sum_split

葉節點依據：sum_split + set_operations_def + forall_intro

對任意互斥事件 A′、C′，A′∪C′ 上的權重和可拆成兩部分之和（sum_split），所以 P(A′∪C′)=P(A′)+P(C′)。這是有限情形的可加性；互斥足以保證這個等式，而不互斥時一般不能保證，S15 給出失敗的例子。重疊部分機率為 0 時，即使兩事件不互斥，等式仍可能成立。



S08 · equivalent操作前

P(S\setminus E)

操作後

1-P(E)

條件：E\subseteq S

規則：L_complement · 依賴：S06, S07

葉節點依據：sum_split + set_operations_def + eq_congruence

依引理 L_complement，補事件的機率是 1 減去原事件的機率；補事件是相對同一個 S 取的。證明在 S08.1、S08.2。



S09 · equivalent操作前

P(\{1,3\})

操作後

w_1+w_3=\tfrac12+\tfrac16=\tfrac46=\tfrac23

條件：無

規則：def_unfold · 依賴：S01, S02, G1

葉節點依據：def_unfold + frac_rules + numeric_evaluation

E={1,3}，依定義加總成員的權重：w_1+w_3=1/2+1/6=3/6+1/6=4/6=2/3。



S10 · implies操作前

\tfrac{|E|}{|S|}=\tfrac24=\tfrac12

操作後

\tfrac12\neq\tfrac23=P(E)

條件：w_1\neq w_2

規則：mko_prob_def · 依賴：S09, G1

葉節點依據：mko_prob_def + numeric_evaluation

若誤用有利結果數除以總結果數，會得 |E|/|S|=2/4=1/2，與正確值 2/3 不同。原因是本模型沒有宣告等可能：w_1=1/2≠1/3=w_2。MKO 明示只有所有結果等可能時才可用 |E|/|S|（等可能情形見 S13）。



S11 · implies操作前

P(S\setminus E)=P(\{2,4\})

操作後

w_2+w_4=\tfrac13+0=\tfrac13=1-\tfrac23

條件：無

規則：def_unfold · 依賴：S08, S09, G1

葉節點依據：def_unfold + L_complement + numeric_evaluation

S∖E={2,4}，直接加總得 1/3+0=1/3；由 L_complement 得 1−2/3=1/3。兩種算法一致，這是對 S09 的交叉核對。



S12 · implies操作前

Z=\{4\}

操作後

Z\neq\varnothing,\quad P(Z)=w_4=0

條件：無

規則：def_unfold · 依賴：S01, S02, G1

葉節點依據：def_unfold + contradiction

Z={4} 含結果 4，所以不是空集合；但 P(Z)=w_4=0。因此 P(E)=0 不能推出 E=∅：非空事件的成員權重若全為 0，機率也是 0（MKO para1）。反方向 E=∅ ⇒ P(E)=0 則由 S05 成立。



S13 · implies操作前

w_s=\tfrac{1}{|S|}\ \text{for all}\ s\in S

操作後

P(E)=\tfrac{|E|}{|S|}

條件：\text{equiprobable}

規則：L_equiprob · 依賴：S01, finite_sum_rules

葉節點依據：L_equiprob + finite_sum_rules

依引理 L_equiprob，若每個權重都等於 1/|S|，則對所有事件 E⊆S 都有 P(E)=|E|/|S|；證明在 S13.1。非均勻模型的個別事件仍可能恰好符合這個等式，不能從單一事件的等式反推權重均勻。例如若改用等可能權重 1/4，則 P({1,3})=2/4=1/2——但那是另一個模型，不是 G1 的模型。



S14 · implies操作前

w'=(\tfrac12,\tfrac13,\tfrac13,0),\quad w''=(\tfrac12,\tfrac23,-\tfrac16,0)

操作後

\sum w'=\tfrac76\neq 1;\quad w''_3=-\tfrac16<0

條件：無

規則：mko_prob_def · 依賴：G3, S01

葉節點依據：mko_prob_def + order_basics + numeric_evaluation

w′ 的權重都非負，但總和 3/6+2/6+2/6+0=7/6≠1，用它會得到 P(S)=7/6，不是機率律。w″ 的總和 3/6+4/6−1/6+0=6/6=1，但 w″_3=−1/6<0，會給出 P({3})<0。兩者都違反 MKO 的合法性條件，所以都不能用來計算機率。合法性兩個條件缺一不可。



S15 · implies操作前

A=\{1,2\},\ C=\{2,3\},\ A\cap C=\{2\}

操作後

P(A)+P(C)=\tfrac56+\tfrac12=\tfrac43\neq 1=P(A\cup C)

條件：A\cap C\neq\varnothing

規則：def_unfold · 依賴：G2, S01, S06

葉節點依據：def_unfold + numeric_evaluation

A、C 有共同結果 2，不互斥。P(A)=1/2+1/3=5/6，P(C)=1/3+1/6=1/2，和為 4/3；但 A∪C={1,2,3}，P(A∪C)=1/2+1/3+1/6=1。差 1/3 正是共同結果 2 的權重被加了兩次。所以 S07 的互斥條件不能省略。



S16 · implies操作前

\text{model}\ (S,\mathcal{P}(S),w)

操作後

\text{legal};\ P(\varnothing)=0,\ P(S)=1;\ P(\{1,3\})=\tfrac23\neq\tfrac12;\ P(\{4\})=0;\ w',w''\ \text{illegal}

條件：無

規則：and_intro_elim · 依賴：S04, S05, S06, S08, S09, S10, S12, S14, S15

葉節點依據：and_intro_elim

彙整：G1 的權重合法；P(∅)=0、P(S)=1、互斥可加、補事件 P(S∖E)=1−P(E)；P({1,3})=2/3，而非計數公式的 1/2；{4} 非空但機率為 0；w′、w″ 不合法；不互斥時不能直接相加。







## 局部子步與引理

S08.1 · implies操作前

E\subseteq S

操作後

E\cap(S\setminus E)=\varnothing,\quad E\cup(S\setminus E)=S

條件：E\subseteq S

規則：set_operations_def · 依賴：set_operations_def, subset_def

葉節點依據：set_operations_def + subset_def + set_extensionality

S∖E 的元素不在 E 中，所以兩者互斥。S 的元素要嘛在 E、要嘛不在 E（因此在 S∖E），所以聯集包含 S；反過來 E⊆S、S∖E⊆S，所以聯集正好是 S。



S08.2 · equivalent操作前

P(S)=P(E)+P(S\setminus E)

操作後

P(S\setminus E)=1-P(E)

條件：無

規則：eq_congruence · 依賴：S08.1, S07, S06

葉節點依據：eq_congruence + add_inverse + sum_split

由 S08.1 與 S07，P(S)=P(E)+P(S∖E)；由 S06，左邊是 1。兩邊同減 P(E) 得 P(S∖E)=1−P(E)。S08.1 與 S08.2 合起來證得引理 L_complement。



S13.1 · equivalent操作前

\sum_{s\in E}\tfrac{1}{|S|}

操作後

|E|\cdot\tfrac{1}{|S|}=\tfrac{|E|}{|S|}

條件：|S|\geq 1

規則：finite_sum_rules · 依賴：finite_sum_rules, S01

葉節點依據：finite_sum_rules + frac_rules

若每個 w_s=1/|S|，P(E) 是 |E| 個相同項 1/|S| 之和；依 finite_sum_rules 的常數倍規則（Σ c·1=c·Σ 1），等於 |E|·(1/|S|)=|E|/|S|。S 非空，所以 |S|≥1，分母不為零。這證得引理 L_equiprob。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S04, S05, S06, S08, S09, S10, S12, S14, S15, and_intro_elim — 目標 G：各項結論。足夠條件 H：所列各步的結論；H⇒G 只是合取。H 由定義與精確計算正向證成，沒有把 G 當作前提。
- S15 · premise_audit · def_unfold, numeric_evaluation, S07 — 一個反例（N11 至 N13）說明沒有互斥時加法不成立；不影響 S07 對互斥事件的結論。
- S14 · premise_audit · mko_prob_def, numeric_evaluation, order_basics — 每個候選只需一個條件不成立即被拒絕（N8 至 N10）。
- S13.1 · inverse_equivalence · finite_sum_rules, frac_rules — 常數項的和等於項數乘常數，雙向成立；需要 S 非空（N7 以 |E|=2、|S|=4 為例）。
- S13 · premise_audit · L_equiprob, finite_sum_rules — 計數公式是等可能假設下的推論，不是一般定義；G1 的模型不滿足此假設。
- S12 · premise_audit · def_unfold, S05 — 一個反例即否定「P(E)=0 ⇒ E=∅」這個一般命題。
- S11 · premise_audit · S08, S09, def_unfold — 補事件相對同一個 S={1,2,3,4} 取（N6）；換成別的樣本空間就不能用 1−P(E)。
- S10 · premise_audit · S09, mko_prob_def, numeric_evaluation — 一組不等的權重（N5）就足以說明等可能不成立；兩個數值不同（N4）說明公式在此不適用。
- S09 · inverse_equivalence · def_unfold, frac_rules, numeric_evaluation — 精確有理運算，可重算（N3）。
- S08.2 · inverse_equivalence · eq_congruence, add_inverse — 同減與同加 P(E) 互為反運算；所用的 P(S)=1 來自 S04 的權重驗證。
- S08.1 · premise_audit · set_operations_def, subset_def, set_extensionality — 需要 E⊆S；若 E 含 S 以外的元素，E∪(S∖E) 就不是 S。
- S08 · inverse_equivalence · L_complement — 兩邊是同一個數；引理對每個 E⊆S 成立。
- S07 · premise_audit · sum_split, set_operations_def — 需要 A′∩C′=∅；若有重疊，共同的權重會被加兩次。
- S06 · inverse_equivalence · def_unfold, S04 — 展開定義並代入 S04，雙向成立。
- S05 · inverse_equivalence · sum_split, finite_sum_rules — 空和的值是定義的一部分，兩式表示同一個數。
- S04 · inverse_equivalence · frac_rules, numeric_evaluation — 通分與約分互為反向，精確有理運算可重算（N1、N2）；不使用近似小數。
- S03 · premise_audit · order_basics, numeric_evaluation — 非負是合法性的一半；總和條件另在 S04 檢查。
- S02 · premise_audit · subset_def, G1 — 逐一檢查有限集合的元素，是完整檢查。
- S01 · premise_audit · G1, mko_prob_def — 此步只寫出定義與合法性條件，不推出新事實。





## 錯誤控制與反例

未宣告等可能不能用 |E|/|S|MKO 指出的第一個誤解是未聲明等可能就套「有利結果數除以總結果數」。本模型中 P({1,3})=2/3，而 |E|/|S|=1/2（S09、S10）。計數公式只是等可能假設下的推論（S13）。

機率為零不代表事件為空MKO 指出的第二個誤解是由 P(E)=0 推出 E=∅。{4} 非空但 P({4})=w_4=0（S12）。只有反方向 E=∅ ⇒ P(E)=0 成立（S05）。

先驗證權重；相加要互斥計算前要確認每個權重非負且總和恰為 1：w′ 總和 7/6、w″ 有負權重，都不能用（S14）。互斥時可直接相加，不互斥時則一般不能直接相加（若重疊部分機率為 0，等式仍可成立）。例如：{1,2} 與 {2,3} 的機率相加得 4/3，大於 1（S15）。補事件要相對同一個 S 取（S11）。


- P({1,3})=|{1,3}|/|S|=2/4=1/2 → reject — 結果不等可能（w_1=1/2≠1/3=w_2）；正確值是 w_1+w_3=2/3。
- P({4})=0，所以 {4} 是空事件 → reject — {4} 含結果 4，非空；它的機率為 0 只因 w_4=0。
- w′=(1/2,1/3,1/3,0) 的權重都非負，所以是合法模型 → reject — 總和是 7/6≠1，會給出 P(S)=7/6。
- P({1,2}∪{2,3})=P({1,2})+P({2,3})=4/3 → reject — 兩事件共有結果 2，不互斥；正確值 P({1,2,3})=1。





## 結論與限制

權重 (1/2,1/3,1/6,0) 非負且總和為 1，構成 S={1,2,3,4} 上的合法機率律。由定義得 P(∅)=0、P(S)=1、互斥事件可加、P(S∖E)=1−P(E)。P({1,3})=2/3，不是 |E|/|S|=1/2（本模型不等可能）；P({2,4})=1/3=1−2/3；{4} 非空但 P({4})=0。(1/2,1/3,1/3,0) 總和 7/6、(1/2,2/3,−1/6,0) 含負權重，都不合法。


- sum_split 作為前置規則使用，是 finite_sum_rules 經重新編號的結果，本稿沒有寫出重新編號的細節。
- 本稿不推論真實實驗的機率，也不處理獨立性、條件機率或一般測度論的事件族（MKO para2）。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 1207c52eb66a78870472c59aac433a88d6d082ed767b689177fc213797904c1d
- original source SHA-256: 1207c52eb66a78870472c59aac433a88d6d082ed767b689177fc213797904c1d
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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