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.
Best Answer
At one point in our paper Degree of Satisfiability in Heyting algebras, Bumpus and I end up showing the following:
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.