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

This made my day.

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!