Probability on finite sample spaces: validating a weight model, computing event probabilities and complements

Goal and scope

Let S={1,2,3,4} with the full powerset as event family and weights w_1=1/2, w_2=1/3, w_3=1/6, w_4=0. Verify that this is a legal finite probability model; prove from the definition the identities P(∅)=0 and P(S)=1, additivity for disjoint events, and the complement identity P(S∖E)=1−P(E); compute P({1,3}) and explain why it differs from |E|/|S|; show that {4} is nonempty yet has probability 0; and decide that the candidate weights (1/2,1/3,1/3,0) and (1/2,2/3,−1/6,0) are both illegal.

Within the MKO's scope: a nonempty finite sample space, the full powerset as event family, exact rational weights (nonnegative, summing to exactly one), and event probability as the sum of member weights. It infers no probabilities of real experiments and does not treat independence, conditional probability or general measure theory (MKO para2); the canonical MKO and its English edition are not changed.

Givens and symbols

• finite_sum_rules
• set_operations_def
• subset_def
• order_basics
• frac_rules
• numeric_evaluation

• G1 — S={1,2,3,4}, four distinct outcome labels; event family F=𝒫(S); weights w_1=1/2, w_2=1/3, w_3=1/6, w_4=0 (MKO assumptions a1, a2).
• G2 — Events to compute: E={1,3}, Z={4}, and A={1,2}, C={2,3}.
• G3 — Candidate weights for comparison: w′=(1/2,1/3,1/3,0) and w″=(1/2,2/3,−1/6,0), for outcomes 1, 2, 3, 4 in order.

• S — the sample space {1,2,3,4}
• \mathcal{P}(S) — the full powerset of S (the event family)
• w_s — the rational weight of outcome s
• P(E)=\sum_{s\in E}w_s — the probability of the event E
• S\setminus E — the complement of E relative to S
• |E| — the number of elements of E

Rules and sources

• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{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 — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_prob_def · cited — Let S be a nonempty finite sample space and F=𝒫(S) its event family. Assign rational weights w_s≥0 to all s∈S with Σ_(s∈S)w_s=1. For E⊆S, P(E)=Σ_(s∈E)w_s. The formula P(E)=|E|/|S| applies only when all outcomes are explicitly equiprobable. · mko-probability
• sum_split · prerequisite — Splitting a finite sum: for numbers w_s on a finite set S and disjoint subsets A, C⊆S, Σ_{s∈A∪C} w_s=Σ_{s∈A} w_s+Σ_{s∈C} w_s; the sum over the empty set is 0. This follows from finite_sum_rules by reindexing.
• L_complement · lemma — In a legal finite model, P(S∖E)=1−P(E) for every event E⊆S.
• L_equiprob · lemma — If every w_s=1/|S|, then P(E)=|E|/|S| for every E⊆S.

Main derivation

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

Substeps and lemmas

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

Reverse audits

• S16 · sufficient_goal_reduction · S04, S05, S06, S08, S09, S10, S12, S14, S15, and_intro_elim — Goal G: all the stated conclusions. Sufficient condition H: the conclusions of the listed steps; H⇒G is just conjunction. H is proved forwards from the definition and exact computation; G is never used as a premise.
• S15 · premise_audit · def_unfold, numeric_evaluation, S07 — One counterexample (N11 to N13) shows that additivity fails without disjointness; it does not affect S07's conclusion for disjoint events.
• S14 · premise_audit · mko_prob_def, numeric_evaluation, order_basics — Each candidate is rejected as soon as one condition fails (N8 to N10).
• S13.1 · inverse_equivalence · finite_sum_rules, frac_rules — A sum of a constant equals the number of terms times the constant, valid both ways; it needs S nonempty (N7 illustrates with |E|=2 and |S|=4).
• S13 · premise_audit · L_equiprob, finite_sum_rules — The counting formula is a consequence of the equiprobability assumption, not the general definition; the model of G1 does not satisfy that assumption.
• S12 · premise_audit · def_unfold, S05 — One counterexample refutes the general claim 'P(E)=0 ⇒ E=∅'.
• S11 · premise_audit · S08, S09, def_unfold — The complement is taken relative to the same S={1,2,3,4} (N6); in another sample space 1−P(E) could not be used.
• S10 · premise_audit · S09, mko_prob_def, numeric_evaluation — One pair of unequal weights (N5) suffices to show equiprobability fails; the two different values (N4) show the formula does not apply here.
• S09 · inverse_equivalence · def_unfold, frac_rules, numeric_evaluation — Exact rational arithmetic, recomputable (N3).
• S08.2 · inverse_equivalence · eq_congruence, add_inverse — Subtracting and adding P(E) undo each other; the fact P(S)=1 used here comes from the weight check in S04.
• S08.1 · premise_audit · set_operations_def, subset_def, set_extensionality — It needs E⊆S; if E contained elements outside S, E∪(S∖E) would not be S.
• S08 · inverse_equivalence · L_complement — Both sides are the same number; the lemma holds for every E⊆S.
• S07 · premise_audit · sum_split, set_operations_def — It needs A′∩C′=∅; with an overlap the common weights would be added twice.
• S06 · inverse_equivalence · def_unfold, S04 — Unfolding the definition and substituting S04 works both ways.
• S05 · inverse_equivalence · sum_split, finite_sum_rules — The value of an empty sum is part of the definition; both expressions name the same number.
• S04 · inverse_equivalence · frac_rules, numeric_evaluation — Bringing to a common denominator and reducing are inverse moves, and the exact rational arithmetic is recomputable (N1, N2); no approximate decimals are used.
• S03 · premise_audit · order_basics, numeric_evaluation — Nonnegativity is half of legality; the sum condition is checked separately in S04.
• S02 · premise_audit · subset_def, G1 — The elements of these finite sets are checked one by one; this is a complete check.
• S01 · premise_audit · G1, mko_prob_def — This step only states the definition and the legality conditions; no new fact is derived.

Error controls and negative controls

Without declared equiprobability, |E|/|S| is not available

The first error named in the MKO is to use 'favourable outcomes over total outcomes' without declared equiprobability. In this model P({1,3})=2/3, while |E|/|S|=1/2 (S09, S10). The counting formula is only a consequence of the equiprobability assumption (S13).

Probability zero does not mean the event is empty

The second error named in the MKO is to infer E=∅ from P(E)=0. {4} is nonempty but P({4})=w_4=0 (S12). Only the other direction, E=∅ ⇒ P(E)=0, holds (S05).

Validate the weights first; add only disjoint events

Before computing, confirm that every weight is nonnegative and the weights sum to exactly 1: w′ sums to 7/6 and w″ has a negative weight, so neither may be used (S14). Disjoint events may be added directly; overlapping events generally may not (though the equality still holds when their intersection has probability zero). For example, adding the probabilities of {1,2} and {2,3} gives 4/3, more than 1 (S15). Complements are taken relative to the same S (S11).

• P({1,3})=|{1,3}|/|S|=2/4=1/2 → reject — The outcomes are not equiprobable (w_1=1/2≠1/3=w_2); the correct value is w_1+w_3=2/3.
• P({4})=0, so {4} is the empty event → reject — {4} contains the outcome 4 and is nonempty; its probability is 0 only because w_4=0.
• w′=(1/2,1/3,1/3,0) has only nonnegative weights, so it is a legal model → reject — The weights sum to 7/6≠1, which would give P(S)=7/6.
• P({1,2}∪{2,3})=P({1,2})+P({2,3})=4/3 → reject — The events share the outcome 2 and are not disjoint; the correct value is P({1,2,3})=1.

Result and limitations

The weights (1/2,1/3,1/6,0) are nonnegative and sum to 1, so they form a legal probability law on S={1,2,3,4}. From the definition, P(∅)=0, P(S)=1, disjoint events add, and P(S∖E)=1−P(E). P({1,3})=2/3, not |E|/|S|=1/2 (this model is not equiprobable); P({2,4})=1/3=1−2/3; {4} is nonempty but P({4})=0. The weights (1/2,1/3,1/3,0), summing to 7/6, and (1/2,2/3,−1/6,0), with a negative weight, are both illegal.

• sum_split is used as a prerequisite; it follows from finite_sum_rules by reindexing, and the details of the reindexing are not written out here.
• This guide infers no probabilities of real experiments and does not treat independence, conditional probability or event families of general measure theory (MKO para2).

Verification and source binding

14 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)