§ Intuitionstic logic as a Heyting algebra

open sets form a Heyting Algebra, which is a lattice plus an implication operator. So it's stronger than a lattice, but weaker than a boolean algebra. Formally, a Heyting algebra over a set $X$ is a collection $(L, \lor, \land, \Rightarrow)$ where $(X, \lor, \land)$ form a lattice, and $\Rightarrow$ obeys the axiom

In any topological space $(U, \tau)$ ( $U$ for universe set) the open sets of that space form a Heyting 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:

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:

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:

Alternatively, we can use the fact that in regular boolean algebra:

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
  already included!]
================== A -> B

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

curry, uncurry are the adjunction/isomorphism:

((c,a) -> b) ~ (c -> (a -> b))

Read this as:

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

if and only if

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

That is, we have "read" curry/uncurry as:

which was the definition of $\Rightarrow$ we wanted!

§ References

• Email by Olaf Klinke on haskell-cafe