I thougt about propositional logic and boolean algebras and how propositional logic is (at least from one point of view) not really about $\land,\lor,\neg,...$ but about boolean operators, i.e. n-ary functions which map $0$-$1$-sequences of length $n$ into $\{0,1\}$, and how to use a finite subset of those (base) to encode all of them.

With boolean algebras it's a little bit similar, one way to think of them is as a mathematical structure associated with a set $X\supseteq\{0,1\}$ which enlarges each boolean operator $f$ to an $X$-valued operator ${\cal X}(f)$ such that this operation is compatible with function composition, i.e. $${\cal X}(f)({\cal X}(g_1),\dots,{\cal X}(g_n))={\cal X}(f(g_1,\dots,g_n)).$$ But any boolean algebra is also a lattice (via $\land$ and $\lor$) and any lattice structure can be described as partial order. I just wonder if it's also possible to describe the partial order on a boolean algebra in terms which do not prioritize the operations $\land$ and $\lor$.


A poset is the underlying poset of a Heyting algebra iff as a category, it has finite products, finite coproducts, and is cartesian closed. Every Boolean algebra is a Heyting algebra, so these are necessary conditions for a poset to be the underlying poset of a Boolean algebra. Heyting algebras are to intuitionistic logic as Boolean algebras are to propositional logic; see, for example, this blog post.

The remaining question is which Heyting algebras are Boolean algebras. In every Heyting algebra we can define a negation operator

$$\neg x = (x \Rightarrow \bot)$$

where $\Rightarrow$ denotes implication / exponential and $\bot$ denotes false / the initial object. There is a natural map $x \to \neg \neg x$, and a Heyting algebra is a Boolean algebra iff this natural map is always an isomorphism, or in other words, iff double negation holds.

| cite | improve this answer | |
  • $\begingroup$ Thanks so much for the answer and the link to your blog post, this was exactly the question I set out to answer (how to invent intuitionistic logic), the thing with boolean algebra was just something I came across. So that is really helpful :) $\endgroup$ – fweth Dec 4 '15 at 22:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.