---
tag: STPBXBKSZP
kind: statement
role: theorem
name: Boolean prime ideal theorem
msc: ["03E25", "06E05", "03G05"]
uses: [06GKBTAA5E, SR56KCFYYS, 0HTGB13FE2, 04RXTQA5ZA]
about: [0XADJKM699]
sources:
  - url: https://en.wikipedia.org/wiki/Boolean_prime_ideal_theorem
same_as:
  wikidata: Q872088
  wikipedia: Boolean prime ideal theorem
---

## Statement

Let $B$ be a [[Boolean algebra|06GKBTAA5E]] with operations $\wedge$, $\vee$, $\neg$, least element $0$ and greatest element $1$.
An ideal of $B$ is a set $I \subseteq B$ such that $0 \in I$, $a \vee b \in I$ for all $a, b \in I$, and $a \in I$ whenever $a \le b$ and $b \in I$.
An ideal $I$ is prime if $1 \notin I$ and, for each $a \in B$, either $a \in I$ or $\neg a \in I$.
Then each ideal $I$ of $B$ with $1 \notin I$ is contained in a prime ideal of $B$.

## Remarks

In ZFC the proof applies [[Zorn's lemma|04RXTQA5ZA]] to the ideals that contain $I$ and omit $1$.
A maximal one $P$ is prime: if $a \notin P$ and $\neg a \notin P$, then the ideals generated by $P \cup \set{a}$ and by $P \cup \set{\neg a}$ both contain $1$, and this forces $1 \in P$.
The theorem is usually abbreviated BPI.
By duality, BPI is equivalent to the ultrafilter lemma: each filter on a set extends to an [[ultrafilter|SR56KCFYYS]].
Over ZF, BPI follows from the [[axiom of choice|0HTGB13FE2]] but does not imply it.
Over ZF, BPI is equivalent to the compactness theorem of first-order logic and to Stone's representation theorem for Boolean algebras.
Example: in the power set Boolean algebra of a set $X$, with $x \in X$, the family of subsets of $X$ that do not contain $x$ is a prime ideal.

## Explanations

### L1 human

A Boolean algebra is an abstract version of the algebra of subsets of a set, with "and", "or" and "not".
A prime ideal is a way to split the algebra into "small" elements and "large" elements, so that each element or its complement is small.
The theorem says that such a split always exists, extending any consistent choice of small elements.
It needs a weak form of the axiom of choice.

### L2 human

BPI is the choice principle behind many compactness arguments.
It gives the ultrafilter lemma, the compactness theorem of first-order logic, and the representation of every Boolean algebra as an algebra of clopen sets of a Stone space.
It also gives [[Tychonoff's theorem|0JTRSJKCFB]] for products of compact Hausdorff spaces, though not for arbitrary compact spaces, which needs full choice.
So it sits strictly between ZF and ZFC, and it is a common test of how much choice a theorem really needs.