Event independence: deciding by the product rule, with the conditional form, complements and a zero-probability event

Goal and scope

Fair-die model: Ω={1,2,3,4,5,6}, each outcome with mass 1/6. Let A={2,4,6}, B={1,2,3,4}, D={1,3,5} and Z=∅. (1) Decide by the product definition whether A and B are independent, and with P(B)>0 check P(A|B)=P(A). (2) Prove that independence of A and B implies independence of A and Bᶜ, and check it numerically. (3) Decide whether the mutually exclusive events A and D are independent. (4) Decide whether A and the zero-probability event Z are independent, and explain why the conditional form cannot be used.

Works inside the MKO's scope: the sample space, exact rational masses and event subsets are fully explicit (assumption a1); only independence of two events is treated (assumption a2), and a three-event example appears only in the error and negative controls, to show that pairwise independence does not stand in for mutual independence. Infinite sample spaces and independence of random variables (the next node) are not treated, and the canonical MKO and its English edition are not changed.

Givens and symbols

• prob_axioms
• set_operations_def
• frac_rules
• mul_inverse_nonzero
• numeric_evaluation

• G1 — Ω={1,2,3,4,5,6}, the events are all subsets of Ω, each outcome has mass m(ω)=1/6, and P(E)=Σ_{ω∈E} m(ω).
• G2 — A={2,4,6}, B={1,2,3,4}, D={1,3,5} and Z=∅, all subsets of the same Ω.

• \Omega=\{1,2,3,4,5,6\} — the sample space
• m(\omega)=\tfrac16 — the mass of each outcome
• P(E) — the probability of E, the sum of masses in E
• A,B,D,Z — the four given events; Z=∅
• B^c — the complement of B in Ω
• P(A\mid B) — conditional probability, defined only when P(B)>0

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.
• 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.
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• 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_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• 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.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• 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.
• 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.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_event_indep_def · cited — In one probability space, A and B are independent iff P(A∩B)=P(A)P(B). If P(B)>0, this is equivalent to P(A|B)=P(A). For P(B)=0, an undefined conditional probability must not replace the product definition. · mko-event-independence
• cond_prob_def · cited — In a finite sample space, for P(B)>0 define P(A|B)=P(A∩B)/P(B); if P(B)=0 this conditional probability is left undefined, even when B is nonempty. · mko-conditional-probability
• point_mass_sum · prerequisite — In a finite model the probability of an event is the sum of the masses of its outcomes: P(E)=Σ_{ω∈E} m(ω); the empty sum is 0.
• L_cond_equiv · lemma — If P(B)>0, then P(A∩B)=P(A)P(B) ⇔ P(A|B)=P(A).
• L_complement · lemma — In one probability space, if P(A∩B)=P(A)P(B), then P(A∩Bᶜ)=P(A)P(Bᶜ).

Main derivation

\Omega=\{1,2,3,4,5,6\},\ m(\omega)=\tfrac16

P(E)=\sum_{\omega\in E}m(\omega)=\tfrac{|E|}{6},\ \ P(\Omega)=6\cdot\tfrac16=1

P(A),\ A=\{2,4,6\}

P(A)=\tfrac36=\tfrac12

P(B),\ B=\{1,2,3,4\}

P(B)=\tfrac46=\tfrac23

A\cap B

\{2,4\}

P(A\cap B)=P(\{2,4\})

P(A\cap B)=\tfrac26=\tfrac13

P(A)P(B)

\tfrac12\cdot\tfrac23=\tfrac13

P(A\cap B)=\tfrac13=P(A)P(B)

A,\ B\ \text{independent}

P(B)=\tfrac23>0

P(A\mid B)=\frac{P(A\cap B)}{P(B)}=\frac{1/3}{2/3}=\tfrac12

P(A\mid B)=\tfrac12,\ P(A)=\tfrac12,\ P(B)>0

P(A\mid B)=P(A),\ \text{consistent with}\ P(A\cap B)=P(A)P(B)

P(A\cap B)=P(A)P(B)

P(A\cap B^c)=P(A)P(B^c)

B^c=\{5,6\},\ A\cap B^c=\{6\}

P(A\cap B^c)=\tfrac16=\tfrac12\cdot\tfrac13=P(A)P(B^c)

A\cap D=\{2,4,6\}\cap\{1,3,5\}=\varnothing

P(A\cap D)=0\neq\tfrac14=P(A)P(D)\ \Rightarrow\ A,D\ \text{not independent}

A\cap D=\varnothing,\ P(A)>0,\ P(D)>0

P(A\cap D)=0<P(A)P(D)\ \Rightarrow\ A,D\ \text{not independent}

Z=\varnothing,\ P(Z)=0

P(A\cap Z)=0=P(A)\cdot 0=P(A)P(Z)\ \Rightarrow\ A,Z\ \text{independent};\ P(A\mid Z)\ \text{undefined}

\text{S07},\ \text{S09},\ \text{S10},\ \text{S12},\ \text{S14}

A\perp B;\ A\perp B^c;\ A\not\perp D;\ A\perp Z

Substeps and lemmas

P(A\mid B)=P(A)

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

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

P(A\cap B)=P(A)P(B)

A

A=(A\cap B)\cup(A\cap B^c),\ \ (A\cap B)\cap(A\cap B^c)=\varnothing

A=(A\cap B)\sqcup(A\cap B^c)

P(A)=P(A\cap B)+P(A\cap B^c)

P(A\cap B^c)=P(A)-P(A\cap B)

P(A\cap B^c)=P(A)-P(A)P(B)=P(A)(1-P(B))=P(A)P(B^c)

Reverse audits

• S15 · sufficient_goal_reduction · S07, S10, S12, S14, and_intro_elim — Goal G is the conjunction of the four decisions; the sufficient condition H is S07, S10, S12 and S14, with H⇒G by conjunction introduction; H is proved forwards from the givens and G is never used as a premise.
• S14 · premise_audit · mko_event_indep_def, cond_prob_def, mul_zero — The decision uses only the product definition and u·0=0 (N10); it does not use P(A|Z) and does not claim it equals any number.
• S13 · premise_audit · order_basics, prob_axioms — It needs u>0, w>0 ⇒ uw>0 (order axioms) and P(∅)=0; no converse is claimed, that is, dependent events need not be mutually exclusive.
• S12 · premise_audit · mko_event_indep_def, S02, numeric_evaluation — Denying independence needs only that the product equation fails for this pair (N9).
• S11 · premise_audit · S01, S10, numeric_evaluation — This is an independent recomputation for these numbers (N7, N8), not a proof of L_complement.
• S10.3 · premise_audit · S10.2, distributive, prob_axioms — The only hypothesis used is the product equation itself; there is no division, so neither P(B)>0 nor P(A)>0 is needed.
• S10.2 · premise_audit · S10.1, prob_axioms — Additivity needs the two parts to be disjoint, established in S10.1; if they overlapped the sum would double count.
• S10.1 · inverse_equivalence · set_operations_def, set_extensionality — x∈A ⇔ x∈A∩B or x∈A∩Bᶜ, so both sides have the same elements; disjointness comes from B∩Bᶜ=∅.
• S10 · premise_audit · S07, L_complement — It needs the product equation of S07; the converse (from A⊥Bᶜ back to A⊥B) is also true since (Bᶜ)ᶜ=B, but this step does not use it.
• S09.2 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — Multiplying by P(B) and by 1/P(B) undo each other, under the condition P(B)≠0.
• S09.1 · inverse_equivalence · cond_prob_def, def_unfold — Unfolding and folding the definition undo each other, given P(B)>0.
• S09 · premise_audit · S08, L_cond_equiv — The lemma needs P(B)>0, established in S03. The main criterion remains the product form of S07; the conditional form is only an equivalent check when the denominator is positive.
• S08 · premise_audit · S03, S05, cond_prob_def, frac_rules — The premise is P(B)>0; without it the division is not allowed (see S14). The value is checked by N6.
• S07 · inverse_equivalence · mko_event_indep_def, S05, S06 — The MKO's definition is an 'iff', so the step holds both ways: independence also gives back the product equation.
• S06 · inverse_equivalence · frac_rules, numeric_evaluation — Exact rational arithmetic; both sides have the same value (N5), so it holds both ways.
• S05 · inverse_equivalence · point_mass_sum, frac_rules — As in S03, the reduction is valid both ways (N4).
• S04 · inverse_equivalence · set_operations_def, set_extensionality — Checking each of the six outcomes of Ω, both sides contain the same elements, so they are equal by extensionality.
• S03 · inverse_equivalence · point_mass_sum, frac_rules — Reducing a fraction is an equal rewriting, 2/3=4/6, valid both ways (N3).
• S02 · inverse_equivalence · point_mass_sum, numeric_evaluation — Backward: 1/2=3/6 is the sum of the three masses of A, so both expressions name the same number (N2).
• S01 · premise_audit · G1, point_mass_sum — It only states the model and checks that the total is 1 (N1); every later probability is computed with this P, and numbers from another model may not be mixed in.

Error controls and negative controls

Mutual exclusion does not imply independence

The first misconception identified in the MKO is to treat mutually exclusive events as independent. Mutual exclusion is the set relation A∩D=∅; independence is the probability relation P(A∩D)=P(A)P(D). S12 and S13 show that two mutually exclusive events of positive probability are never independent, because 0<P(A)P(D).

Use the product definition when P(B)=0

The conditional form P(A|B)=P(A) is equivalent to independence only when P(B)>0 (S09). When P(B)=0, P(A|B) is undefined: it cannot be 'computed' and compared, nor set to P(A) by fiat. The product definition still applies and shows that a zero-probability event is independent of every event (S14).

Pairwise independence does not ensure mutual independence

This guide handles only two events. For three events, pairwise independence does not imply mutual independence: toss two fair coins, Ω′={HH,HT,TH,TT}, E₁=first is heads, E₂=second is heads, E₃=both agree. Every pairwise intersection is {HH} with probability 1/4=(1/2)(1/2), but P(E₁∩E₂∩E₃)=1/4≠1/8=(1/2)³.

• A={2,4,6} and D={1,3,5} share no outcome, so they are independent → reject — P(A∩D)=0 but P(A)P(D)=1/4; the product equation fails.
• P(A|∅) is undefined, so independence of A and ∅ cannot be decided → reject — The main criterion is the product definition: P(A∩∅)=0=P(A)·0, so A and ∅ are independent.
• When P(B)=0 we may agree that P(A|B)=P(A) and then decide independence by the conditional form → reject — The MKO explicitly forbids replacing the product definition by an undefined conditional probability; when P(B)=0 only P(A∩B)=P(A)P(B) may be used.
• In the two-coin example E₁, E₂, E₃ are pairwise independent, so the three are mutually independent → reject — P(E₁∩E₂∩E₃)=1/4 while P(E₁)P(E₂)P(E₃)=1/8.

Result and limitations

In the fair-die model P(A∩B)=1/3=P(A)P(B), so A={2,4,6} and B={1,2,3,4} are independent, and since P(B)>0, P(A|B)=1/2=P(A). The same equation implies that A and Bᶜ are independent, checked as 1/6=(1/2)(1/3). The mutually exclusive A and D={1,3,5} are not independent (0≠1/4). A and the zero-probability event ∅ are independent by the product definition, while the conditional probability P(A|∅) is undefined and may not be used.

• Mutual independence of three events appears only as a counterexample in the error controls, without a full definition or theorem; it lies outside the MKO's scope.
• N11 and N12 belong to the two-coin model Ω′, separate from the die model Ω; their numbers must not be mixed.

Verification and source binding

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

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

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