# Event: deciding what counts as an event under the full event family and under a coarser one [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-event/) 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-event-01 · production-20261019-adopted-96 ## Goal and scope Roll a die once, S={1,2,3,4,5,6}. (1) In the finite elementary model F=𝒫(S), show that E={2,4,6} is an event, and decide whether E occurs when the observed outcome is 4 and when it is 3; distinguish the outcome 4 from the event {4}; describe the empty and the sure event. (2) In the general model (S,F₀) with F₀={∅,O,E,S} and O={1,3,5}: prove that F₀ is an event family (σ-algebra) on S, and prove {6}∉F₀, so although S is finite and {6}⊆S, {6} is not an event in this model. Works inside the MKO's scope: the sample space S is explicit (assumption a1), and the event family of each model is explicit (assumption a2). The event family of a general model follows the standard σ-algebra definition (prerequisite sigma_algebra_def). No probability values are assigned; infinite sample spaces and Lean's MeasurableSet are not treated; the canonical MKO and its English edition are not changed. ## Givens and symbols - subset_def - set_operations_def - set_extensionality - powerset_def - sigma_algebra_def - G1 — Experiment: roll a six-sided die once and record the number shown; sample space S={1,2,3,4,5,6} (assumption a1). - G2 — Model M1: the finite elementary model, with the explicit event family F=𝒫(S) (assumption a2). - G3 — Model M2: the general model (S,F₀), with the explicit F₀={∅,O,E,S}, where O={1,3,5} and E={2,4,6} (for example when only the parity of the roll can be observed) (assumption a2). - S — the sample space of one roll - \mathcal{P}(S) — the full event family of all subsets of S - F_0 — the coarser event family {∅,O,E,S} - E,\ O — the even outcomes, the odd outcomes - \omega — the observed outcome - S\setminus X — the complement of X in S ## Rules and sources - subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B). - 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. - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - 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. - 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_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true. - 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. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility. - exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a. - exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x). - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_event_def · cited — The finite elementary model in this entry explicitly uses the full event family F=P(S), so an event E may be any subset of S. In a general model (S,F), whether S is finite or infinite, an event must belong to F. Event E occurs when the observed outcome belongs to E. · mko-event - powerset_def · prerequisite — Power set: X∈𝒫(S) if and only if X⊆S. - sigma_algebra_def · prerequisite — Event family (σ-algebra): a family F of subsets of S is an event family on S if S∈F; S∖X∈F whenever X∈F; and the union of any countably many (including finitely many) members of F belongs to F. - L_F0_unions · lemma — The union of any countably many members of F₀ belongs to F₀. ## Main derivation S01 · definitionBefore \text{one roll of a die} After S=\{1,2,3,4,5,6\},\ E=\{2,4,6\},\ O=\{1,3,5\} Conditions: none Rule: def_intro · Uses: G1, G2, G3 Leaf basis: def_intro + mko_event_def State the sample space S first, then name the two subsets used below: E, the even outcomes, and O, the odd outcomes. By the MKO, the sample space and the event family must be specified before events are listed; the event families of the two models are stated in G2 and G3. S02 · impliesBefore E=\{2,4,6\},\ O=\{1,3,5\} After E\subseteq S,\ O\subseteq S Conditions: none Rule: subset_def · Uses: S01 Leaf basis: subset_def + forall_intro The three elements 2, 4, 6 of E all lie in S, and so do the three elements 1, 3, 5 of O; this checks every element of these finite sets, so by the subset definition E⊆S and O⊆S. S03 · equivalentBefore E\subseteq S After E\in\mathcal{P}(S)=F Conditions: F=\mathcal{P}(S) Rule: powerset_def · Uses: G2, S02 Leaf basis: powerset_def + eq_replace In model M1, F=𝒫(S). By the definition of power set, X∈𝒫(S) exactly when X⊆S; by S02, E⊆S, so E∈F and E is an event in M1. By the MKO, passing directly from 'is a subset' to 'is an event' is allowed only when F=𝒫(S) is explicitly adopted. S04 · impliesBefore \omega=4,\quad \omega=3 After 4\in E\Rightarrow E\ \text{occurs};\quad 3\notin E\Rightarrow E\ \text{does not occur} Conditions: E\in F Rule: mko_event_def · Uses: S01, S03 Leaf basis: mko_event_def + def_unfold By the MKO, E occurs when the observed outcome belongs to E. With ω=4, 4 is one of the listed elements of E, so E occurs; with ω=3, 3 is not in {2,4,6}, so E does not occur. Whether an event occurs is decided by whether the observed outcome belongs to it. S05 · impliesBefore 4\in S,\ \{4\}\subseteq S After 4\ \text{is an outcome},\ \{4\}\in F,\ 4\neq\{4\} Conditions: F=\mathcal{P}(S) Rule: powerset_def · Uses: S01, S03 Leaf basis: powerset_def + subset_def + mko_event_def 4 is an element of S, an elementary outcome; {4} is a subset of S and, in M1, belongs to F by the definition of power set, so it is an event. They have different types: 4 is a number, {4} is a set, and 4≠{4}. When the outcome 4 is observed, the event {4} occurs; E={2,4,6} contains three outcomes, so an event is in general not a single outcome. S06 · impliesBefore \varnothing\subseteq S,\ S\subseteq S After \varnothing,\ S\in F;\ \varnothing\ \text{never occurs},\ S\ \text{always occurs} Conditions: F=\mathcal{P}(S) Rule: powerset_def · Uses: S01, G2 Leaf basis: powerset_def + subset_def + mko_event_def ∅⊆S (there is no element to check) and S⊆S, so both are events in M1. No ω belongs to ∅, so the empty event never occurs; every observed outcome belongs to S (the sample space contains every possible outcome), so the sure event S always occurs. These names do not assign probability values. S07 · impliesBefore F_0=\{\varnothing,O,E,S\} After F_0\subseteq\mathcal{P}(S),\ S\in F_0 Conditions: none Rule: sigma_algebra_def · Uses: G3, S02, S06 Leaf basis: sigma_algebra_def + subset_def Move to model M2 and check the σ-algebra definition clause by clause. First clause: the four members ∅, O, E, S of F₀ are all subsets of S (S02, S06), so F₀ is a family of subsets of S; and S is one of the members of F₀. S08 · impliesBefore S\setminus\varnothing,\ S\setminus S,\ S\setminus E,\ S\setminus O After S,\ \varnothing,\ O,\ E\ \in F_0 Conditions: none Rule: set_operations_def · Uses: S07 Leaf basis: set_operations_def + set_extensionality Compute the complement in S of each member of F₀: S∖∅=S and S∖S=∅; S∖E consists of the elements of S not in {2,4,6}, namely {1,3,5}=O; likewise S∖O=E. All four complements lie in F₀, so F₀ is closed under complement and the second clause of the σ-algebra definition holds. S09 · impliesBefore E=\{2,4,6\},\ O=\{1,3,5\} After E\cup O=S,\ E\cap O=\varnothing Conditions: none Rule: set_operations_def · Uses: S01 Leaf basis: set_operations_def + set_extensionality + numeric_evaluation Of the six elements of S, 2, 4, 6 are in E and 1, 3, 5 are in O, and each element lies in exactly one of them. So E∪O=S and E∩O=∅; count check 3+3=6. From here on E and O are called the atoms of F₀. S10 · impliesBefore (X_i)_{i\in\mathbb{N}}\ \text{with each}\ X_i\in F_0 After \bigcup_{i\in\mathbb{N}}X_i\in F_0;\ F_0\ \text{is an event family on }S Conditions: none Rule: L_F0_unions · Uses: S07, S08, S09 Leaf basis: sigma_algebra_def + set_operations_def + case_analysis + exists_elim By Lemma L_F0_unions (proved in S10.1 to S10.3), the union of any countably many members of F₀ lies in F₀; finite unions are a special case (take the remaining terms to be ∅). Together with S07 and S08, all three clauses of the σ-algebra definition hold, so F₀ is an event family on S and M2 is a legitimate general model. S11 · impliesBefore \{6\}\ \text{compared with}\ \varnothing,\ O,\ E,\ S After \{6\}\notin F_0 Conditions: none Rule: set_extensionality · Uses: S01, G3 Leaf basis: set_extensionality + case_analysis For {6} to belong to F₀ it must equal one of the four members. {6}≠∅ since 6∈{6}; {6}≠O since 6∉O; {6}≠E since 2∈E but 2∉{6}; {6}≠S since 1∈S but 1∉{6}. None is equal, so {6}∉F₀. S12 · impliesBefore \{6\}\subseteq S,\ |S|=6,\ \{6\}\notin F_0 After \{6\}\ \text{is not an event of}\ (S,F_0) Conditions: F_0\ \text{an event family} Rule: mko_event_def · Uses: S10, S11 Leaf basis: mko_event_def + powerset_def By the MKO, in a general model (S,F) an event must belong to F. {6}⊆S and S has only 6 elements, but {6}∉F₀ (S11), so {6} is not an event in M2; 'the roll is 6' cannot be treated as an event in M2. Finiteness of S does not make every subset an event automatically; in M1, {6} is an event only because M1 explicitly adopts F=𝒫(S). S13 · impliesBefore E\in F_0,\ \omega=4 After E\ \text{is an event of}\ (S,F_0)\ \text{and occurs} Conditions: none Rule: mko_event_def · Uses: S04, S10 Leaf basis: mko_event_def E is a member of F₀, so E is an event in M2 as well; with ω=4, 4∈E and E occurs. The same set E is an event in both models, while {6} is an event only in M1: whether a set is an event depends on the event family, not only on S. S14 · impliesBefore \text{models}\ (S,\mathcal{P}(S))\ \text{and}\ (S,F_0) After E\ \text{event in both};\ \{6\}\ \text{event in}\ (S,\mathcal{P}(S))\ \text{only} Conditions: none Rule: and_intro_elim · Uses: S03, S04, S05, S06, S10, S12, S13 Leaf basis: and_intro_elim Collect the results: in M1, E is an event that occurs for ω=4 and not for ω=3 (S03, S04); the outcome 4 differs from the event {4} (S05); ∅ never occurs and S always occurs (S06). In M2, F₀ is an event family (S10), E is still an event (S13), but {6} is not (S12). ## Substeps and lemmas S10.1 · impliesBefore X\in F_0 After X=\bigcup\{A\in\{E,O\}\mid A\subseteq X\} Conditions: none Rule: set_extensionality · Uses: S09 Leaf basis: set_extensionality + subset_def + set_operations_def Check the four members of F₀ one by one: no atom is contained in ∅ (E and O are nonempty), and the union of the empty family is ∅; the only atom contained in E is E (1∈O but 1∉E), with union E; likewise only O is contained in O; the atoms contained in S are E and O, with union E∪O=S (S09). So each X∈F₀ equals the union of the atoms it contains. S10.2 · equivalentBefore x\in\bigcup_{i}X_i After x\in\bigcup\{A\in\{E,O\}\mid\exists i,\ A\subseteq X_i\} Conditions: X_i\in F_0\ \text{for all}\ i Rule: set_operations_def · Uses: S10.1 Leaf basis: set_operations_def + eq_replace + exists_intro + exists_elim x belongs to the union ⇔ x∈X_i for some i ⇔ (by S10.1) for some i and some atom A⊆X_i, x∈A ⇔ x belongs to some atom that is contained in some X_i. Swapping the order of the two existential quantifiers does not change the truth value. So the countable union equals the union of these atoms. S10.3 · impliesBefore \{A\in\{E,O\}\mid\exists i,\ A\subseteq X_i\} After \bigcup_i X_i\in\{\varnothing,E,O,S\}=F_0 Conditions: none Rule: case_analysis · Uses: S10.2, S09 Leaf basis: case_analysis + set_operations_def The selected family of atoms is a subfamily of {E,O}, so there are only four possibilities: the empty family, {E}, {O} and {E,O}, whose unions are ∅, E, O and E∪O=S, all of which belong to F₀. S10.1 to S10.3 together prove Lemma L_F0_unions. ## Reverse audits - S14 · sufficient_goal_reduction · S03, S04, S05, S06, S10, S12, S13, and_intro_elim — Goal G is the conjunction of the problem's conclusions; each is proved forwards by the listed steps, and this step only forms the conjunction; G is never used as a premise. - S13 · premise_audit · mko_event_def, S10 — It needs E∈F₀ (from the list in G3) and F₀ legitimate (S10); occurrence is decided as in S04. - S12 · premise_audit · mko_event_def, S10, S11 — It needs F₀ to be a legitimate event family (S10); otherwise M2 would not be a model and the conclusion would be meaningless. - S11 · premise_audit · set_extensionality, G3 — F₀ is a finite list, so comparing with each member is a complete check; each inequality has a witness element. - S10.3 · premise_audit · S10.2, S09, case_analysis — The four cases exhaust the subfamilies of {E,O}; the argument holds for any countable family, regardless of how many sets it lists. - S10.2 · inverse_equivalence · S10.1, set_operations_def, exists_intro, exists_elim — Each move is an equivalence: the definition of union, the set equality of S10.1, and swapping existential quantifiers; so both sides have the same elements. - S10.1 · premise_audit · S09, set_extensionality, subset_def — All four members of F₀ are checked, a complete enumeration; the property is claimed only for members of F₀. - S10 · premise_audit · S07, S08, L_F0_unions, sigma_algebra_def — Each of the three clauses is supplied by one step; it is not claimed that F₀ contains every subset of S (S11 shows the opposite). - S09 · premise_audit · set_operations_def, set_extensionality — Each of the six elements of S is checked, a complete enumeration. - S08 · premise_audit · set_operations_def, set_extensionality, sigma_algebra_def — F₀ has only four members, so computing each is a complete check. - S07 · premise_audit · sigma_algebra_def, S02 — Only the first clause is checked here; the other two are in S08 and S10. - S06 · premise_audit · powerset_def, subset_def, mko_event_def, G1 — S always occurring needs the completeness of the sample space (G1); P(∅)=0 or P(S)=1 is not claimed, since that needs a separately given probability model. - S05 · premise_audit · powerset_def, subset_def, mko_event_def — {4}⊆S because its only element 4 is in S; {4}∈F relies on F=𝒫(S) in M1 and need not hold in M2 (S11 treats the similar set {6}). - S04 · premise_audit · mko_event_def, S03 — It needs E to be an event (S03); occurrence is defined only for events. No probability value is claimed. - S03 · inverse_equivalence · powerset_def, G2 — The power-set definition is two-way; but this equivalence links subsets with events only in a model with F=𝒫(S). - S02 · premise_audit · subset_def — A complete enumeration, not a sample; the converse S⊆E is not claimed (1∉E). - S01 · premise_audit · G1, G2, G3, def_intro — This step only records data and names, deriving no new fact; S and both event families are explicit, as assumptions a1 and a2 require. ## Error controls and negative controls An event is not a single outcomeThe MKO names the mistake of treating an event as a single outcome. 4 is an element of S (an outcome), {4} is a subset of S (an event), and 4≠{4}; E={2,4,6} contains three outcomes (S05). 'E occurs' means the observed outcome belongs to E, not that it equals E. Specify the sample space and event family firstThe MKO warns against listing events before the sample space or event family is specified. The question 'is {6} an event?' has no fixed answer: it is in M1 and is not in M2 (S12). So S and F must be stated before any events are listed. A finite S does not make every subset an eventThe MKO names another mistake: assuming a finite sample space makes every subset measurable. In M2, S has only 6 elements and F₀ is a legitimate event family (S07, S08, S10), yet {6}∉F₀. Every subset is an event only when F=𝒫(S) is explicitly adopted. - S is finite, so {6} is an event in every model (S,F) → reject — In M2, {6}∉F₀ (S11, S12). - The event E={2,4,6} is the outcome 4 → reject — E is a set of three outcomes; 4 is only one of its elements (S05). - When 3 is observed, the event E={2,4,6} occurs → reject — 3∉E, so E does not occur (S04). - E is an event, so P(E)=1/2 → reject — Neither model in this guide assigns probabilities; being an event does not fix a probability value. - F₀ does not contain {6}, so F₀ is not an event family → reject — All three σ-algebra clauses are checked in S07, S08 and S10; an event family need not contain singletons. ## Result and limitations In the finite elementary model F=𝒫(S), E={2,4,6} is an event; it occurs when 4 is observed and not when 3 is observed; the outcome 4 differs from the event {4}; the empty event never occurs and the sure event always occurs. In the general model (S,F₀), F₀={∅,{1,3,5},{2,4,6},S} is an event family and E is still an event, but {6}∉F₀, so although S is finite and {6}⊆S, {6} is not an event. - The event family of a general model uses the standard σ-algebra definition (sigma_algebra_def) as a prerequisite; the MKO itself only requires events to belong to the explicit F. - N1 and N2 check by remainders that 4 is even and 3 is odd; they are cross-checks only, and the argument relies on the lists of E and O. ## Verification and source binding 5 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 5f67b035b93e0779d5d9d9a91ef38849d1d4aa6bcd00b2c987bd6528a63147cd - original source SHA-256: 5f67b035b93e0779d5d9d9a91ef38849d1d4aa6bcd00b2c987bd6528a63147cd - 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-event-01.json)