nLab Phoa's principle

Idea

Phoa’s principle is a principle used to axiomatize Sierpinski space in synthetic topology and synthetic domain theory. Phoa’s principle is also called the Phoa principle in Bauer & Taylor 2009.

Phoa’s principle is named after Wesley Phoa.

Definition

Let $L$ be a 01-bounded semilattice, that is, a semilattice with an absorbing element. Phoa’s principle states that every endofunction $f:L \to L$ is monotonic and the precomposition function $h \mapsto h \circ i:L^L \to L^\mathbb{2}$ by the embedding $i:\mathbb{2} \hookrightarrow L$ of the booleans into $L$ is an embedding.

If $L$ is a distributive lattice, then Phoa’s principle is equivalent to the linear interpolation condition that for all endofunctions $f:L \to L$ and elements $x \in L$:

$$f(x) = f(\top) \wedge (x \vee f(\bot))$$

Properties

There are many types of distributive lattices for which non-trivial such distributive lattices cannot satisfy Phoa’s principle.

Theorem

Suppose $L$ is a distributive lattice $L$ with an endpoint-swapping endofunction $\neg:L \to L$, where $\neg(\top) = \bot$ and $\neg(\bot) = \top$. Then the only such distributive lattice $L$ for which Phoa’s principle holds is the trivial Heyting algebra.

Proof

Applying the function $x \mapsto \neg x$ to the linear interpolation condition for the distributive lattice yields

$$\neg x = \neg (\top) \wedge (x \vee \neg \bot) = \bot \wedge (x \vee \top) = \bot$$

Substituting $\bot$ into the equation yields

$$\neg \bot = \top = \bot$$

which is precisely the condition that $L$ be a trivial such distributive lattice.

Lemma

Suppose $L$ is a Heyting algebra for which Phoa’s principle holds. Then $L$ is the trivial Heyting algebra.

Proof

$L$ being a Heyting algebra implies that $L$ has a Heyting implication $x, y \mapsto x \to y$ and thus a Heyting negation function $x \mapsto \neg x$ defined by $\neg x \coloneqq x \to \bot$ such that $\neg(\top) = \bot$ and $\neg(\bot) = \top$. Hence, by the first theorem, $L$ is the trivial Heyting algebra if Phoa’s principle holds.

Theorem

Suppose $L$ is a De Morgan algebra for which Phoa’s principle holds. Then $L$ is the trivial De Morgan algebra.

Proof

$L$ being a De Morgan algebra implies that $L$ has an involution $x \mapsto \neg x$ such that $\neg(\top) = \bot$ and $\neg(\bot) = \top$. Hence, by the first theorem, $L$ is the trivial De Morgan algebra if Phoa’s principle holds.

Lemma

Suppose $L$ is a finite distributive lattice for which Phoa’s principle holds. Then $L$ is the trivial distributive lattice.

Proof

If $L$ is a finite distributive lattice, then there are many such functions $f:L \to L$ such that $f(\top) = \bot$ and $f(\bot) = \top$ definable using the universal property of the finite set with $n$ elements. Hence, by the first theorem, $L$ is the trivial distributive lattice if Phoa’s principle holds.

Lemma

There are no distributive lattices $L$, whose carrier set is the set of natural numbers, for which Phoa’s principle holds.

Proof

Suppose that $L$ is a distributive lattice whose carrier set is the set of natural numbers. Then there are many such functions $f:L \to L$ such that $f(\top) = \bot$ and $f(\bot) = \top$ definable using the universal property of the natural numbers. Hence, by the first theorem, $L$ is the trivial distributive lattice if Phoa’s principle holds, which contradicts that the carrier set of $L$ is the set of natural numbers.

Examples

• In Pos the category of posets and monotonic functions, Phoa’s principle holds for the boolean domain $\mathbb{2}$.

• In synthetic Stone duality, Phoa’s principle holds for the type of open propositions $\mathrm{Open}$.

• In synthetic domain theory and synthetic topology, Phoa’s principle holds for a dominance $\Omega$.

Related concepts

• distributive lattice

• flat distributive lattice

• 01-bounded semilattice

• sigma-frame

• directed univalence

• domain theory, synthetic domain theory

• synthetic quasi-coherence

• Sierpinski space

References

• Wesley Phoa: Domain theory in realizability toposes, PhD thesis, Trinity College, Cambridge (November 1990) [lfcs:91/ECS-LFCS-91-171, pdf]

• Paul Taylor, The Fixed Point Property in Synthetic Domain Theory, Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, [doi:10.1109/LICS.1991.151640, pdf]

• Andrej Bauer, Paul Taylor, The Dedekind reals in abstract Stone duality, Mathematical Structures in Computer Science 19 4 (2009) 757-838 [doi:10.1017/S0960129509007695, pdf]

• Davorin Lešnik, Synthetic Topology and Constructive Metric Spaces [arXiv:2104.10399]

• Davorin Lešnik, “Synthetic Topology”. In: Douglas Bridges, Hajime Ishihara, Michael Rathjen, Helmut Schwichtenberg, editors, Handbook of Constructive Mathematics, Encyclopedia of Mathematics and its Applications, Cambridge University Press, pp. 445 - 482, 04 May 2023. [doi:10.1017/9781009039888.018]

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)

• Thierry Coquand, Freek Geerligs, Hugo Moeneclaey, Directed Univalence in Synthetic Stone Duality, unfinished draft; LaTeX documents can be found here.

• Jonathan Sterling, Baby steps in higher domain theory, talk at Homotopy Type Theory and Computing – Classical and Quantum, Center for Quantum and Topological Systems (video)

• Leoni Pugh, Jonathan Sterling, When is the partial map classifier a Sierpiński cone? (arXiv:2504.06789)

• Jonathan Sterling, Lingyuan Ye, Domains and Classifying Topoi (arXiv:2505.13096)

• Fredrik Bakke, Jonathan Sterling, Mark Damuni Williams, Lingyuan Ye, The Synthetic Sierpiński Cone (arXiv:2605.00773)

• Constructive subtleties about the Sierpinski Space, Mathematics StackExchange. (web)