I am looking for examples of proofs or constructions that rely on a Heyting algebra. Furthermore, said examples must use the fact that Heyting algebras can be considered semantics for IPC, but be outside the study scope of IPC.

An example that does not fit the above criteria would be the construction of the Lindenbaum algebra from propositional formulae, because it is used to prove completeness.

An example that might fit the above criteria would be the fact that every Heyting algebra can be transformed into a collection of open sets of a topological space. I don't know if this construction can be actually used outside of IPC, in conjuction with the fact that it also acts as semantics for IPC.

The way I see it, any construction that is available for all Heyting algebras will not fit the criteria. Maybe something that is dependent on the inner structure of a particular one.

Edit: Adding some motivation/clarification.
Didactic reasons. When a student of logic is first introduced to the concepts of syntax/semantics, it is difficult to provide examples of actually using the formal language, usually because the language is so limited to keep the simplicity. Classical propositional calculus does not offer such a richness of models as IPC, so I thought that at least with IPC semantics we can do something other than just derivations.

  • $\begingroup$ Would something like this count: proving $\operatorname{int}(\operatorname{cl}(\operatorname{int}(\operatorname{cl}(U)))) = \operatorname{int}(\operatorname{cl}(U))$ for open $U$ in a topological space, using the fact that $\operatorname{int}\circ \operatorname{cl}$ is double negation in the Heyting algebra of open sets, and $\lnot\lnot$ is idempotent? $\endgroup$ Nov 8, 2022 at 22:18
  • $\begingroup$ Yes, but I am looking for more fancy stuff. $\endgroup$
    – Jason
    Nov 8, 2022 at 22:20

1 Answer 1


At one point in our paper Degree of Satisfiability in Heyting algebras, Bumpus and I end up showing the following:

A finite $T_0$ topological space can have at most twice as many clopen sets as non-closed open sets.

However, an infinite $T_0$ space that has more clopen sets than non-closed opens is discrete (and therefore has no non-closed open sets at all!).

These are interesting statements about topological spaces that have nothing to do with IPC. But as you might guess from the title, they arise for algebraic/logical reasons, as corollaries of results about Heyting algebras, by using the fact that the opens of a topological space always form a Heyting algebra.

  • $\begingroup$ So my intuition that a universal construction would not be helpful was incorrect. $\endgroup$
    – Jason
    Nov 8, 2022 at 23:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .