Conditional probability in finite models: positive denominators, the two directions and null conditioning events

Goal and scope

In the finite model on S={1,2,3,4,5,6} with weights w=(1,2,3,2,4,0)/12, let A={2,3}, B={3,4,5,6} and Z={6}. Validate the model, compute P(A|B) and P(B|A), compare them with the equiprobable count ratio |A∩B|/|B| and with the product P(A)P(B), and decide whether P(A|Z) is defined.

Works inside the MKO's scope: a nonempty finite sample space, the full power set as event family, normalized nonnegative rational weights. Defines P(A|B)=P(A∩B)/P(B) only when P(B)>0, and proves a small additivity lemma (P(E′)=P(E)+P(E′∖E) for E⊆E′) to show 0≤P(A|B)≤1. Leaves conditioning on null events undefined; does not discuss independence, Bayes' theorem or infinite sample spaces; does not change the canonical MKO or its English edition.

Givens and symbols

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

• G1 — S={1,2,3,4,5,6}, event family F=𝒫(S), weights 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). The model is not declared equiprobable.
• G2 — Events A={2,3}, B={3,4,5,6}, Z={6}.
• G3 — To do: validate the model and the events; find P(A|B) and P(B|A); compare with |A∩B|/|B| and P(A)P(B); decide P(A|Z).

• S — the sample space {1,2,3,4,5,6}
• w(s) — the weight of the sample point s
• P(E) — the probability Σ_{s∈E} w(s) of the event E
• P(A\mid B) — the conditional probability of A given B, i.e. C(A,B)
• A^{c} — S∖A

Rules and sources

• prob_axioms · prerequisite — Probability axioms: P(A)≥0; P(Ω)=1; the probability of a (countable) union of pairwise disjoint events is the sum of their probabilities. Hence P(∅)=0 and P(Aᶜ)=1−P(A).
• 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).
• 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.
• 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.
• 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.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_cond_prob_def · cited — In a nonempty finite sample space S with event family F=𝒫(S) and normalized nonnegative rational weights, let A,B⊆S with P(B)>0. Define C(A,B)=P(A|B)=P(A∩B)/P(B). If P(B)=0, this entry leaves that conditional probability undefined, even when B is nonempty. · mko-conditional-probability
• weight_model · prerequisite — Finite weighted model: w:S→ℚ with w(s)≥0 for every s and Σ_{s∈S} w(s)=1; the probability of an event E⊆S is P(E)=Σ_{s∈E} w(s) (the empty sum is 0).
• L_split · lemma — In a finite weighted model, if E⊆E′⊆S then P(E′)=P(E)+P(E′∖E), and hence P(E)≤P(E′).

Main derivation

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}

Substeps and lemmas

E\subseteq E'\subseteq S

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

Reverse audits

• S15 · sufficient_goal_reduction · S01, S07, S11, S12, S13, S14, and_intro_elim — Goal G: the items of the task. Sufficient condition H: the conclusions of the listed steps; H⇒G is just conjunction, H is proved forwards from G1 and G2, and G is never used as a premise.
• S14 · premise_audit · mko_cond_prob_def, mul_inverse_nonzero — The verdict rests only on P(Z)=0; nonemptiness is not enough for conditioning. Nothing is claimed about how other theories handle conditioning on null events.
• S13 · premise_audit · frac_rules, numeric_evaluation — Only an exact comparison of two rationals is needed; no conclusion about independence is drawn here.
• S12 · premise_audit · mko_cond_prob_def, weight_model — One pair of unequal weights shows the model is not equiprobable; this step only rules out a wrong method.
• S11 · premise_audit · mko_cond_prob_def, set_operations_def, frac_rules — Each direction needs its own positive denominator (MKO paragraph three); the intersection is symmetric, but the denominators may not be swapped.
• S10 · premise_audit · L_split, S03, S06, frac_rules — This is an independent consistency check, not needed for deriving P(A|B).
• S09.1 · premise_audit · weight_model, set_operations_def, finite_sum_rules, order_basics — It needs the disjoint split and nonnegative weights; with negative weights the inequality part would fail.
• S09 · premise_audit · L_split, order_basics — Dividing by a positive number keeps the inequality direction, so P(B)>0 is needed; the lemma is proved in S09.1.
• S08 · inverse_equivalence · frac_rules — The fraction rules are equalities when the denominators are nonzero, so this holds both ways.
• S07 · inverse_equivalence · frac_rules, mul_inverse_nonzero — Backward: P(A|B)·P(B)=(1/3)·(3/4)=1/4=P(A∩B) (N5); multiplying and dividing by 3/4 undo each other, given 3/4≠0.
• S06 · inverse_equivalence · weight_model, frac_rules — An exact evaluation, holding both ways.
• S05 · inverse_equivalence · set_operations_def, set_extensionality — The two sets have the same elements, so by set equality it holds both ways.
• S04 · premise_audit · mko_cond_prob_def, order_basics — What is needed is P(B) strictly positive, not merely B nonempty (see S14).
• S03 · inverse_equivalence · weight_model, frac_rules, numeric_evaluation — An exact rational evaluation; both sides are the same number.
• S02 · premise_audit · subset_def — An element-by-element check suffices; no converse is claimed.
• S01 · premise_audit · weight_model, numeric_evaluation — Both conditions (nonnegativity, total 1) must be checked; every later probability depends on this step.

Error controls and negative controls

Nonempty does not mean positive probability

The first misconception named by the MKO is treating nonempty as positive probability. Z={6} is nonempty, but w(6)=0, so P(Z)=0 and one cannot condition on Z (S14). Before conditioning, what must be checked is P(B)>0 (S04), not B≠∅.

Conditioning on a null event does not give zero

The second misconception identified in the MKO is answering zero for a null conditioning event. The formula for P(A|Z) has denominator 0, which has no inverse, so P(A|Z) is undefined in this entry; writing 0 or 1 is wrong.

The two directions must not be confused

The third misconception identified in the MKO is confusing the two directions. P(A|B)=1/3 has denominator P(B), while P(B|A)=3/5 has denominator P(A) (S07, S11); they differ, and each needs its own positive-denominator check. Likewise, conditional probability is not P(A)P(B)=5/16 (S13), nor, in a non-equiprobable model, the count ratio 1/4 (S12).

• Z={6} is nonempty, so P(A|Z) is defined → reject — P(Z)=w(6)=0; the MKO requires a strictly positive denominator.
• P(Z)=0, so P(A|Z)=0 → reject — With denominator 0 the expression is undefined, not 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 — The model is not equiprobable (w(5)=4/12, w(6)=0); the correct value is 3/9=1/3.
• P(A|B)=P(A)P(B)=5/16 → reject — The conditional probability is P(A∩B)/P(B)=1/3, not a product of two probabilities.

Result and limitations

The weights (1,2,3,2,4,0)/12 form a valid finite model. P(B)=3/4>0 and P(A∩B)=1/4, so P(A|B)=1/3; P(A)=5/12>0, so P(B|A)=3/5, and the two directions differ. Neither the equiprobable count ratio 1/4 nor the product P(A)P(B)=5/16 is P(A|B). Z={6} is nonempty but P(Z)=0, so P(A|Z) is undefined in this entry.

• This guide does not discuss independence; S13 only compares numbers and makes no claim about whether A and B are independent.
• Conditioning on null events is handled elsewhere in other theories (for example via limits or measure-theoretic conditional expectation), outside this entry's scope.

Verification and source binding

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

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

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