Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Boolean algebra and Boolean ultrafilter

Definition

A Boolean algebra is a set B with distinguished elements 0,1∈B, binary operations ∧,∨:B×B→B and a unary operation ¬:B→B, such that for all a,b,c∈B:

  • (B,∧,1) and (B,∨,0) are commutative monoids (associativity and the identities a∧1=a, a∨0=a);
  • the absorption laws hold: a∧(a∨b)=a and a∨(a∧b)=a;
  • the distributive laws hold: a∧(b∨c)=(a∧b)∨(a∧c) and a∨(b∧c)=(a∨b)∧(a∨c);
  • the complement laws hold: a∧¬a=0 and a∨¬a=1.

The trivial Boolean algebra is the one-element algebra {0}, in which 0=1; it is allowed here, and it corresponds to the empty Stone space in Stone space and clopen algebra.

A Boolean homomorphism φ:B→B′ is a map with φ(0)=0, φ(1)=1, φ(a∧b)=φ(a)∧φ(b), φ(a∨b)=φ(a)∨φ(b) and φ(¬a)=¬φ(a) for all a,b.

A proper filter in B is a subset F⊆B with

  1. 1∈F and 0∉F;
  2. a,b∈F implies a∧b∈F;
  3. a∈F and a≤b (meaning a∧b=a) imply b∈F.

A Boolean ultrafilter is a proper filter that is maximal with respect to inclusion among proper filters.

The complement dichotomy and two-valued homomorphisms

The following two facts are used repeatedly below, and are proved here rather than assumed. Let U⊆B be a proper filter.

Dichotomy. U is an ultrafilter if and only if for every a∈B exactly one of a∈U and ¬a∈U holds.

If U is an ultrafilter and a∉U, then ¬a∈U: if also ¬a∉U, the family U′:={b:b≥a∧u for some u∈U} is a proper filter strictly containing U — it is a filter by construction, it contains a and hence is strictly larger, and it is proper because a∧u≠0 for every u∈U (were a∧u=0 then u≤¬a and ¬a∈U by upward closure, contrary to assumption), so 0∉U′; this contradicts maximality. The two alternatives are exclusive because a∧¬a=0∉U.

Conversely, suppose U decides every element. If U⊆V is a proper filter and a∈V, then ¬a∉V (else 0=a∧¬a∈V), so ¬a∉U and hence a∈U by the dichotomy applied to U; thus V⊆U and V=U, so U is maximal.

Two-valued homomorphisms. The assignments U↦χU, where χU(a)=1 for a∈U and χU(a)=0 otherwise, and χ↦χ−1({1}), are mutually inverse bijections between Boolean ultrafilters on B and Boolean homomorphisms B→{0,1} with the two-element Boolean algebra as codomain.

That χU is a homomorphism uses the dichotomy: χU(¬a)=1−χU(a) by exclusivity, χU(a∧b)=χU(a)χU(b) because U is closed under ∧ and upward closed, and the identity for ∨ follows from de Morgan and the other two, or directly from the fact that a∨b∈U if and only if a∈U or b∈U (if a∨b∈U and both a∉U and b∉U, then ¬a,¬b∈U, so ¬(a∨b)=¬a∧¬b∈U, contradicting (a∨b)∧¬(a∨b)=0∉U; the converse is upward closure). That χ−1({1}) is an ultrafilter is immediate from the homomorphism identities: it is a proper filter, and it decides each element because χ(a)∈{0,1} forces exactly one of χ(a)=1, χ(¬a)=1.

Remarks

  • Filters are proper by convention, as for filters on a set; the improper family B itself is not a filter here, so "ultrafilter" means a maximal proper filter.
  • The trivial algebra has no ultrafilters and no two-valued homomorphisms. In the one-element algebra 0=1, a proper filter would have to contain 1 and omit 0=1, which is impossible; and a Boolean homomorphism to {0,1} would have to send 1 to 1 and 0=1 to 0, which is also impossible. This matches the empty Stone space under the convention of Stone space and clopen algebra.

Depends on

Used by

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources