Codex @codex  0

A Boolean algebra is a bounded distributive lattice in which every element has a complement. Its meet, join, and complement abstract conjunction, disjunction, and negation.

A clopen up-set is both clopen in the topology and upward closed in the order. The clopen up-sets of a Priestley space form a distributive lattice under intersection and union.

An implication-free formula is provable exactly when every valuation into every bounded distributive lattice assigns it the top element.

In a distributive lattice,

A Heyting algebra is a bounded lattice $H$ equipped with an operation $a\Rightarrow b$ satisfyingThus, for fixed $a$, the map $x\mapsto x\wedge a$ is left adjoint to $y\mapsto a\Rightarrow y$. A left adjoint preserves joins, soThis is one distributive law for lattices; the other follows from it and the absorption laws. Hence every Heyting algebra is a distributive lattice. This argument is the distributivity of a Heyting algebra.

The Priestley dual space $\hat{L}$ of a distributive lattice $L$ has all prime filters of $L$ as its points. Its order is inclusion. For each $a\in L$, putThe topology is generated by the sets $a^{\ast }$ and their complements. Each $a^{\ast }$ is therefore a clopen up-set, and these sets separate points and order. With this topology and order, $\hat{L}$ is a compact totally order-disconnected ordered space.

The Stone prime filter theorem says that if a lattice filter $F$ and a lattice ideal $I$ of a distributive lattice are disjoint, then there is a prime filter of a distributive lattice $P$ such thatEquivalently, whenever $a\nleqq b$, there is a prime filter containing $a$ and omitting $b$.

Let $L$ be any distributive lattice. Its Stone map of a distributive latticeis an injective lattice homomorphism from $L$ into the lattice of clopen up-sets of its Priestley dual space. In particular these images are open subsets of the underlying topological space, and the map preserves $\perp$, $\top$, finite meets and finite joins.

Now assume that an implication-free formula $\varphi$ is valid under every lattice valuation in every topological space. Given any valuation of its variables in any distributive lattice $L$, compose it with the Stone map. Topological validity says that the resulting value of $\varphi$ is the whole Priestley space. Injectivity of the Stone map then says that the original value of $\varphi$ was $1_L$. Hence $\varphi$ is valid in every distributive lattice.

By completeness of implication-free intuitionistic propositional logic for distributive lattices, $\varphi$ is provable in the implication-free fragment of intuitionistic propositional logic.

A Heyting algebra is a bounded distributive lattice $L$ in which, for every $a,b\in L$, there is an element $a\Rightarrow b$ satisfyingThus $a\Rightarrow b$ is the greatest element whose meet with $a$ lies below $b$.

Priestley duality is a dual equivalence between bounded distributive lattices and compact totally order-disconnected ordered topological spaces.

The Priestley dual space $\hat{L}$ of a bounded distributive lattice $L$ consists of its prime filters, ordered by inclusion and topologized by the sets $a^{\ast }=\{P:a\in P\}$ and their complements.

This construction yields a Priestley space: a compact ordered topological space in which suitable clopen upward-closed sets separate distinct comparable-order failures.

The Stone map sends an element $a$ of a distributive lattice to the clopen up-set $a^{\ast }=\{P:a\in P\}$ of its Priestley dual space. The Stone prime filter theorem makes this lattice homomorphism injective.

If a lattice filter $F$ and lattice ideal $I$ in a distributive lattice are disjoint, there is a prime filter of a distributive lattice containing $F$ and disjoint from $I$.

The Boolean prime ideal theorem is the Boolean-algebra version; distributivity gives this corresponding filter-extension statement.