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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-conditional-probability/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



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

S01 · impliesBefore

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

After

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

Conditions: none

Rule: weight_model · Uses: G1, weight_model

Leaf basis: weight_model + finite_sum_rules + numeric_evaluation

MKO assumption a1 requires a valid model: every weight is a nonnegative rational and the total is 1. Item by item, 1/12, 2/12, 3/12, 2/12, 4/12 and 0 are all ≥0; the total is (1+2+3+2+4+0)/12=12/12=1 (N1). So this is a valid finite weighted model. w(6)=0 is allowed: a sample point may exist with weight zero.



S02 · impliesBefore

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

After

A,B,Z\subseteq S

Conditions: none

Rule: subset_def · Uses: G1, G2, subset_def

Leaf basis: subset_def

Event eligibility: every element of A, B and Z lies in S={1,2,3,4,5,6}, so all three are subsets of S and belong to the event family 𝒫(S).



S03 · equivalentBefore

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

After

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

Conditions: none

Rule: weight_model · Uses: S01, S02, weight_model

Leaf basis: weight_model + finite_sum_rules + frac_rules + numeric_evaluation

MKO paragraph one: first compute the probability mass in B. P(B) is the sum of the weights of the four sample points of B: (3+2+4+0)/12=9/12=3/4 (N2).



S04 · impliesBefore

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

After

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

Conditions: P(B)>0

Rule: mko_cond_prob_def · Uses: S03, mko_cond_prob_def

Leaf basis: mko_cond_prob_def + order_basics

By the MKO, P(A|B) is defined only when P(B)>0. Since 3/4>0, we may condition on B. This check must come before any division.



S05 · equivalentBefore

A\cap B

After

\{3\}

Conditions: none

Rule: set_operations_def · Uses: G2, set_operations_def

Leaf basis: set_operations_def + set_extensionality

x∈A∩B exactly when x∈A and x∈B. The elements of A are 2 and 3: 2∉B and 3∈B. So A∩B={3}.



S06 · equivalentBefore

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

After

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

Conditions: none

Rule: weight_model · Uses: S05, weight_model

Leaf basis: weight_model + frac_rules + numeric_evaluation

The second step of MKO paragraph one: compute the mass in A∩B. A∩B={3}, so P(A∩B)=w(3)=3/12=1/4 (N3).



S07 · equivalentBefore

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

After

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

Conditions: P(B)=\tfrac{3}{4}\neq 0

Rule: mko_cond_prob_def · Uses: S04, S06, mko_cond_prob_def

Leaf basis: mko_cond_prob_def + frac_rules + mul_inverse_nonzero + numeric_evaluation

Finally divide: P(A|B)=(1/4)/(3/4)=(1/4)·(4/3)=1/3 (N4). Dividing by 3/4 needs 3/4≠0, confirmed in S04.



S08 · equivalentBefore

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

After

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

Conditions: 12\neq 0; 9\neq 0

Rule: frac_rules · Uses: S03, S06, frac_rules

Leaf basis: frac_rules + numeric_evaluation

MKO paragraph one: a common positive denominator may be cancelled. Both masses are expressed in twelfths of the same model: P(A∩B)=3/12 and P(B)=9/12; by the fraction rules (3/12)/(9/12)=(3·12)/(12·9)=3/9=1/3 (N6, N7), agreeing with S07. Cancelling this way presupposes that both come from the same validated weight model and that the events are eligible.



S09 · theorem_applicationBefore

A\cap B\subseteq B

After

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

Conditions: P(B)>0

Rule: L_split · Uses: S05, S07, L_split

Leaf basis: weight_model + finite_sum_rules + order_basics + set_operations_def

A∩B⊆B, so by Lemma L_split, P(B)=P(A∩B)+P(B∖(A∩B))≥P(A∩B). Dividing by the positive P(B) gives P(A|B)≤1; numerator and denominator are nonnegative, so P(A|B)≥0. Here 1/4≤3/4 (N18), and 1/3 does lie in [0,1].



S10 · impliesBefore

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

After

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

Conditions: P(B)>0

Rule: L_split · Uses: S03, S06, S07, L_split, G2

Leaf basis: weight_model + set_operations_def + frac_rules + numeric_evaluation

Cross-check: B∖(A∩B)={4,5,6}=Aᶜ∩B, with mass (2+4+0)/12=1/2 (N8). By L_split, P(A∩B)+P(Aᶜ∩B)=1/4+1/2=3/4=P(B) (N9), as it should. P(Aᶜ|B)=(1/2)/(3/4)=2/3 (N10), and adding P(A|B) gives 1 (N11): given B, the conditional probabilities of A and Aᶜ sum to 1.



S11 · impliesBefore

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

After

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

Conditions: P(A)>0

Rule: mko_cond_prob_def · Uses: S06, G1, G2, mko_cond_prob_def

Leaf basis: mko_cond_prob_def + set_operations_def + frac_rules + numeric_evaluation

The other direction needs its own denominator check: P(A)=w(2)+w(3)=(2+3)/12=5/12>0 (N12), so P(B|A) is defined. B∩A=A∩B={3}, and P(B|A)=(1/4)/(5/12)=(1/4)·(12/5)=3/5 (N13). 3/5≠1/3 (N14): conditional probabilities in the two directions generally differ, because their denominators differ.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: mko_cond_prob_def · Uses: S05, S07, G1

Leaf basis: mko_cond_prob_def + weight_model + numeric_evaluation

Treating the model as equiprobable by mistake would give the count ratio |A∩B|/|B|=1/4. But the weights here are unequal (for example w(5)=4/12≠w(6)=0) and no equiprobable model was declared (MKO assumption a2), so the count ratio is not this model's conditional probability; the correct value is 1/3 (N15).



S13 · impliesBefore

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

After

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

Conditions: none

Rule: frac_rules · Uses: S03, S07, S11

Leaf basis: frac_rules + numeric_evaluation

Conditional probability is not P(A) times P(B): P(A)P(B)=(5/12)(3/4)=15/48=5/16 (N16), while P(A|B)=1/3, and the two differ (N17). The correct multiplicative relation is P(A∩B)=P(A|B)·P(B)=(1/3)(3/4)=1/4 (the backward check of S07).



S14 · impliesBefore

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

After

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

Conditions: none

Rule: mko_cond_prob_def · Uses: G1, G2, mko_cond_prob_def, mul_inverse_nonzero

Leaf basis: mko_cond_prob_def + mul_inverse_nonzero + weight_model

Z is nonempty (6∈Z), yet P(Z)=w(6)=0. The MKO states that this entry leaves the conditional probability undefined when P(B)=0, even if B is nonempty. The expression P(A∩Z)/P(Z) has denominator 0, and 0 has no inverse, so P(A|Z) is undefined; the answer is neither 0 nor 1.



S15 · impliesBefore

\text{S01 to S14}

After

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

Conditions: none

Rule: and_intro_elim · Uses: S01, S07, S09, S11, S12, S13, S14

Leaf basis: and_intro_elim

Summary: the model is valid (S01); P(B)=3/4>0 and P(A|B)=1/3 (S07), which lies in [0,1] (S09); P(A)=5/12>0 and P(B|A)=3/5≠1/3 (S11); neither the count ratio 1/4 nor the product 5/16 is P(A|B) (S12, S13); P(Z)=0, so P(A|Z) is undefined (S14).







## Substeps and lemmas

S09.1 · impliesBefore

E\subseteq E'\subseteq S

After

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

Conditions: w(s)\ge 0

Rule: finite_sum_rules · Uses: weight_model, set_operations_def, finite_sum_rules

Leaf basis: weight_model + set_operations_def + finite_sum_rules + order_basics

When E⊆E′, each element of E′ lies in exactly one of E and E′∖E (definition of set operations), and the two are disjoint. So the finite sum Σ_{s∈E′} w(s) splits as Σ_{s∈E} w(s)+Σ_{s∈E′∖E} w(s), that is P(E′)=P(E)+P(E′∖E). Every weight is ≥0, so P(E′∖E)≥0 and P(E)≤P(E′). This proves Lemma L_split.







## 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 probabilityThe 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 zeroThe 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 confusedThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-conditional-probability-01.json)