# Using Heyting algebras outside of Intuitionistic Propositional Calculus.

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.

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.

• 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? Nov 8, 2022 at 22:18
• Yes, but I am looking for more fancy stuff. Nov 8, 2022 at 22:20

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!).