§ 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 XX is a collection (L,,,)(L, \lor, \land, \Rightarrow) where (X,,)(X, \lor, \land) form a lattice, and \Rightarrow obeys the axiom
:LL;(ca)b    c(ab) \Rightarrow: L \rightarrow L; (c \land a) \leq b \iff c \leq (a \Rightarrow b)
In any topological space (U,τ)(U, \tau) ( UU 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:
¬Ainterior(AC) \lnot A \equiv \texttt{interior}(A^C)
We need the interior\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 ¬¬A=A\lnot \lnot A = A. but, more on that later! We write open intervals with round parenthesis:
¬A\lnot A of the above set AA becomes the open interval that is in the interior of AA complement.
--(===)-- A
==]---[== A complement
==)---(== Not A
Now, we can try to ask, when is ¬¬A=U\lnot \lnot A = U (where UU 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:
A=U{1}¬A=interior(Ac)=interior({1})=¬¬A=interior((¬A)c)=interior(c)=interior(U)=U \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¬¬AA \simeq \lnot \lnot A, where AA 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 ¬¬A=A\lnot \lnot A = A. Now, we look at implication. The implication ABA \Rightarrow B is the largest set open CC such that CA=BC \land A = B. In pictures:
---(========)----- A
---------(=====)-- B
---------(==)----- A && B
===)-----(======== A -> B
The reason this is true is that from the definition:
:LL;c(ab)    (ca)breplacing  with = for insight::LL;c=(ab)    (ca)=b \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:
ab=¬aba \Rightarrow b = \lnot a \lor b
to derive A>BA -> 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 ¬ab\lnot a \lor b definition:
  1. aba \leq b (given)
  2. Since aba \leq b, ¬a¬b\lnot a \geq \lnot b, since ¬\lnot reverses inclusion order.
  3. xyx \geq y implies that xpypx \lor p \geq y \lor p for all p, since pp is on both sides.
  4. Specializing to x=¬ax = \lnot a, y=¬by = \lnot b, p=bp = b gives us ¬ab¬bb\lnot a \lor b \geq \lnot b \lor b
  5. ¬bb\lnot b \lor b is universe UU
  6. ¬abU\lnot a \lor b \geq U, which means it's equal to UU (nothing can be greater than UU).
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:
cab    cab c \land a \leq b \iff c \leq a \Rightarrow b
which was the definition of \Rightarrow we wanted!

§ References