A Universe of Sorts

§ 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

\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 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:

\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:

$a \leq b$ (given)
Since $a \leq b$ , $\lnot a \geq \lnot b$ , since $\lnot$ reverses inclusion order.
$x \geq y$ implies that $x \lor p \geq y \lor p$ for all p, since $p$ is on both sides.
Specializing to $x = \lnot a$ , $y = \lnot b$ , $p = b$ gives us $\lnot a \lor b \geq \lnot b \lor b$
$\lnot b \lor b$ is universe $U$
$\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:

c \land a \leq b \iff c \leq a \Rightarrow b

which was the definition of

\Rightarrow

we wanted!

§ References

Email by Olaf Klinke on haskell-cafe

§ Intuitionstic logic as a Heyting algebra

§ a -> b as a contained in b:

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

§ References

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

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