# Representation theorem for Complete Atomic Heyting Algebras

It is well known that within classical logic one can characterize complete atomic boolean algebras as powersets.

Is it possible to provide any characterization/representation theorem for complete atomic heyting algebras?

Edit.

After some very constructive considerations in the comments I discovered that I am interested in an unusual notion of atom. Since the question turned out to be interesting also for people outside my mathematical comfort zone, I will write below two different definitions of atom and I would like to have an answer to my question for both definitions.

Atom (2) is the usual notion of atom, atom (1) should be called infinitary join-irreducible or tiny element.

A discussion that relates the two concepts can be found here as proposition 5.1. In boolean algebras these two definitions coincide.

Some definitions.

Def. In a complete poset $\mathbb{P}$ an atom (1) is an element $p$ such that $$\text{if } p \leq \bigvee_{i \in I} a_i \text{ then } p \leq a_j \text{ for some } j \in I.$$

Def. In a poset $\mathbb{P}$ an atom (2) is a minimal nonzero element.

Def. A subset $A$ of a complete poset $\mathbb{P}$ is (join-)dense if for each element $p$ there is a family of $(a_i)$ in A such that $$p = \bigvee a_i.$$

Def. A complete poset is atomic if the set of its atoms is dense.

• what do you mean by atomic Heyting algebra? A Heyting algebra $\mathbb{A}$ such that for every $a\in\mathbb{A}$ there exists some $b\leq a$ such that $b$ is an atom? (where $b$ is an atom if and only if for all $c\leq b$ $c=b$ or $c=\bot$). Notice that if we define a Heyting algebra $\mathbb{A}$ to be atomic iff every element can be written as a join of atoms then it follows that $\mathbb{A}$ is a Boolean algebra Commented Aug 8, 2018 at 16:31
• This is a very interesting comment. My definition was the second one. How do you prove that claim? Commented Aug 8, 2018 at 18:47
• Let $X$ be the set of atoms. Let $a\in\mathbb{A}$ and let $Y\subset X$ such that $\bigvee Y=a$. For every $b\in X\setminus Y$ we have that $a\land b=\bot$. Therefore $$a\to\bot=\bigvee\{b\in\mathbb{A}\mid a\land b\leq\bot\}\geq\bigvee(X\setminus Y).$$ Therefore $a\lor(a\to\bot)=\bigvee X=\top$, i.e. the law of excluded middle holds Commented Aug 9, 2018 at 12:47
• I am thinking a bit about the other definition. The difference is that a complete atomic boolean algebra is perfect, while a complete atomic Heyting algebra (according to the first definition I gave) is not necessarily perfect. I will think about that a bit more and add something later. Commented Aug 9, 2018 at 16:09
• Your first definition of atom is what is lattice theory is called completely join-prime element, which in Heyting algebras coincide with completely join-irreducible; what you call atomic lattice (a complete poset is a lattice) is actually called atomistic, while atomic just means that every element has an atom below it. But perhaps in other areas there are other conventions... I just tried to clarify since there seems to be some debate in the comments. Commented Aug 10, 2018 at 10:56

Definition atom (2) is closer to the meaning of atom. If these atoms join generate the Heyting algebra then it's not hard to see that the completely distributive lattice is in fact a Boolean algebra. Indeed, let $\mathbb{A}$ be a completely distributive lattice that is join-generated by its atoms. Let $X$ be the set of atoms. Let $a\in\mathbb{A}$ and let $Y\subseteq X$ such that $\bigvee Y=a$. For every $b\in X\setminus Y$ we have that $a\land b=\bot$. Therefore $$a\to\bot=\bigvee\{b\in\mathbb{A}\mid a\land b\leq \bot\}\geq\bigvee(X\setminus Y).$$ Hence $a\lor (a\to\bot)=\bigvee X=\top$, i.e. the law of excluded middle holds.