> It says a Boolean algebra is a "degenerate example" of a bi-Heyting algebra. So: how do bi-Heyting algebras differ? Time to read the works of Cecylia Rauszer!

I understand now where the attempted proof I sketched out falls over: if we let \$$⌐ a := \top \setminus a\$$ then while we have \$$\vdash ⌐ \,⌐ a \to a\$$ but sadly \$$\nvdash a \to ⌐ \, ⌐ a \$$.

Cecylia's logic is fascinating. Here's her [1971 paper](http://matwbn.icm.edu.pl/ksiazki/fm/fm83/fm83120.pdf).

She defines \$$\neg a := a \to \bot \$$, and observes that

$$\vdash \neg\, ⌐ (a \to b) \to \neg\, ⌐ a \to \neg \, ⌐ b .$$

She gives a Hilbert calculus with the rule:

$$\frac{a}{\neg \, ⌐ a}$$

So \$$\neg\, ⌐\$$ is a [modality](https://plato.stanford.edu/entries/logic-modal/)! This is pretty wild.

> Bi-Heyting algebras seem like a natural concept.

I would say so. Thank you so much John for teaching this course!