Event: deciding what counts as an event under the full event family and under a coarser one

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

\text{one roll of a die}

S=\{1,2,3,4,5,6\},\ E=\{2,4,6\},\ O=\{1,3,5\}

E=\{2,4,6\},\ O=\{1,3,5\}

E\subseteq S,\ O\subseteq S

E\subseteq S

E\in\mathcal{P}(S)=F

\omega=4,\quad \omega=3

4\in E\Rightarrow E\ \text{occurs};\quad 3\notin E\Rightarrow E\ \text{does not occur}

4\in S,\ \{4\}\subseteq S

4\ \text{is an outcome},\ \{4\}\in F,\ 4\neq\{4\}

\varnothing\subseteq S,\ S\subseteq S

\varnothing,\ S\in F;\ \varnothing\ \text{never occurs},\ S\ \text{always occurs}

F_0=\{\varnothing,O,E,S\}

F_0\subseteq\mathcal{P}(S),\ S\in F_0

S\setminus\varnothing,\ S\setminus S,\ S\setminus E,\ S\setminus O

S,\ \varnothing,\ O,\ E\ \in F_0

E=\{2,4,6\},\ O=\{1,3,5\}

E\cup O=S,\ E\cap O=\varnothing

(X_i)_{i\in\mathbb{N}}\ \text{with each}\ X_i\in F_0

\bigcup_{i\in\mathbb{N}}X_i\in F_0;\ F_0\ \text{is an event family on }S

\{6\}\ \text{compared with}\ \varnothing,\ O,\ E,\ S

\{6\}\notin F_0

\{6\}\subseteq S,\ |S|=6,\ \{6\}\notin F_0

\{6\}\ \text{is not an event of}\ (S,F_0)

E\in F_0,\ \omega=4

E\ \text{is an event of}\ (S,F_0)\ \text{and occurs}

\text{models}\ (S,\mathcal{P}(S))\ \text{and}\ (S,F_0)

E\ \text{event in both};\ \{6\}\ \text{event in}\ (S,\mathcal{P}(S))\ \text{only}

Substeps and lemmas

X\in F_0

X=\bigcup\{A\in\{E,O\}\mid A\subseteq X\}

x\in\bigcup_{i}X_i

x\in\bigcup\{A\in\{E,O\}\mid\exists i,\ A\subseteq X_i\}

\{A\in\{E,O\}\mid\exists i,\ A\subseteq X_i\}

\bigcup_i X_i\in\{\varnothing,E,O,S\}=F_0

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 outcome

The 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 first

The 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 event

The 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)