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

目標與範圍

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|。

逐步主鏈

(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

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)

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

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

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

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

P(\varnothing)

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

P(S)

\sum_{s\in S}w_s=1

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

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

P(S\setminus E)

1-P(E)

P(\{1,3\})

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

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

\tfrac12\neq\tfrac23=P(E)

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

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

Z=\{4\}

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

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

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

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

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

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

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

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

局部子步與引理

E\subseteq S

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

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

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

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

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

逐步反向審查

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