## § Intuitionstic logic as a Heytig algebra

open sets form a Heytig Algebra, which is a lattice plus an implication operator. So it's stronger than a lattice, but weaker than a boolean algebra. Formally, a Heytig algebra over a set $X$ is a collection $(L, \lor, \land, \Rightarrow)$ where $(X, \lor, \land)$ form a lattice, and $\Rightarrow$ obeys the axiom
$\Rightarrow: L \rightarrow L; (c \land a) \leq b \iff c \leq (a \Rightarrow b)$
In any topological space $(U, \tau)$ ( $U$ for universe set) the open sets of that space form a Heytig algebra. Here, set-union and set-intersection become the lattice join and lattice meet. We define a "weak complement" denoted by $\lnot$ which is defined as:
$\lnot A \equiv \texttt{interior}(A^C)$
We need the $\texttt{interior}$ to make sure that we're left with an open set. Also, this $\lnot$ is not really a complement, since we won't have that $\lnot \lnot A = A$. but, more on that later! We write open intervals with round parenthesis:
    A
--(===)--

$\lnot A$ of the above set $A$ becomes the open interval that is in the interior of $A$ complement.
--(===)-- A
==]---[== A complement
==)---(== Not A

Now, we can try to ask, when is $\lnot \lnot A = U$ (where $U$ is the universe set or the full space). If we consider a set containing a single point, then we will have:
==)(== A
------------ Not A
============ Not (Not A)

in words:
\begin{aligned} &A = U \setminus \{ 1 \} \\ &\lnot A = \texttt{interior}(A^c) = \texttt{interior}(\{ 1 \}) = \emptyset \\ &\lnot \lnot A = \texttt{interior}((\lnot A)^c) = \texttt{interior}(\emptyset^c) = \texttt{interior}(U) = U \\ \end{aligned}
So in some sense, the law of excluded middle is "almost true": It holds that $A \simeq \lnot \lnot A$, where $A$ excludes a set of points of measure zero. This is really interesting, since it gives some sort of oddball probabilistic flavour to things where if we blind ourselves to measure-0 sets, then $\lnot \lnot A = A$. Now, we look at implication. The implication $A \Rightarrow B$ is the largest set open $C$ such that $C \land A = B$. In pictures:
---(========)----- A
---------(=====)-- B
---------(==)----- A && B
===)-----(======== A -> B

The reason this is true is that from the definition:
\begin{aligned} &\Rightarrow: L \rightarrow L; c \leq (a \Rightarrow b) \iff (c \land a) \leq b \\ &\text{replacing \leq with = for insight:} \\ &\Rightarrow: L \rightarrow L; c = (a \Rightarrow b) \iff (c \land a) = b \\ \end{aligned}
Alternatively, we can use the fact that in regular boolean algebra:
$a \Rightarrow b = \lnot a \lor b$
to derive $A -> B$:
---(========)----- A
===)--------(===== NOT A
---------(=====)-- B
[Extend B to everything that doesn't include
more of A than already included]
===)-----(======== NOT A or B = A -> B


#### § a -> b as a contained in b:

We'll show that a -> b is true/top/the full real line if and only if a is contained in b. We can show this using $\lnot a \lor b$ definition:
1. $a \leq b$ (given)
2. Since $a \leq b$, $\lnot a \geq \lnot b$, since $\lnot$ reverses inclusion order.
3. $x \geq y$ implies that $x \lor p \geq y \lor p$ for all p, since $p$ is on both sides.
4. Specializing to $x = \lnot a$, $y = \lnot b$, $p = b$ gives us $\lnot a \lor b \geq \lnot b \lor b$
5. $\lnot b \lor b$ is universe $U$
6. $\lnot a \lor b \geq U$, which means it's equal to $U$ (nothing can be greater than $U$).
We can also show this geometrically:
----------(===)---- A
------(==========) B
----------(===)---- A && B
[Extend B to everything that doesn't include
more of A than already included.
But all of A is
================== A -> B


#### § reading curry, uncurry using a -> b as containment:

curry, uncurry are the adjunction/isomorphism:
((c,a) -> b) ~ (c -> (a -> b))

( c     ,         a)     ->         b
(c intersection a) contained in b

c      ->        (a       ->      b)
c contained in (a implication b)

That is, we have "read" curry/uncurry as:
$c \land a \leq b \iff c \leq a \Rightarrow b$
which was the definition of $\Rightarrow$ we wanted!