Modal Space and Computation

It is an old result of Goedel that we can embed propositional intuitionistic logic (Int) in the classical propositional modal logic S4. This latter logic extends classical propositional logic (Prop) via a modality, [], satisfying the following conditions:

(1) [](p -> q) -> []p -> []q
(2) []p -> p
(3) []p -> [][]p

But in what sense is this result obvious? One route to the reason is provided by knowing that Int has as algebraic models complete Heyting algebras. These are complete lattices in which meet distributes over arbitrary join. Now, a complete boolean algebra is also a complete Heyting algebra. Since complete Boolean algebras form models of Prop, we may expect classical logic to embed into Int. This is indeed the case - it does so via the double negation translation (Glivenko's Theorem): p is provable in Prop if and only if ~~p is provable in Int. But we want to go the other way! That is, we want to embed Int inside of some classically based logic. How to do this?

Let's look at a specific Heyting algebra. Pick your favourite topological space X and let O(X) be the collection of all open sets of X. Then, O(X) is a complete Heyting algebra, with join defined by union and meet almost defined by set intersection. Since O(X) is closed under arbitrary union, we are happy on the join front, but for the meet of arbitrarly many members of O(X), we have to take the interior of the intersection.

Now, O(X) directly forms a model of Int by interpreting conjunction as the interior of intersection, disjunction as union, implication as the subset relation and negation as the interior of the relative complement. It is a theorem that every Boolean algabra is isomorphic to a Boolean algebra of sets. That is, a collection of sets closed under intersection, union and relative complement. So, what we need to do is to add a way of talking about topology to Prop. Have another look at the axioms for S4. What they seem to be saying is that [] forms a (topological) interior operator! This is precisely what we need, since an interior operator uniquely determines a topology of open sets (this is usually stated in terms of the dual notion of a closure operator and holds for a large variety of lattices, not just topological spaces).

So, with our S4 modality, we can build a topology on a Boolean algebra. The Goedel translation then becomes obvious. The only thing we really need to worry about is how to translate a negation. If t is our translation function, then we do this by simply taking t(~p) to be []~t(p). That is, we take it to be the interior of the relative complement!

This topological interpretations of things is very neat and leads to lots of nice things. But we can be a bit brash and crazy and ask what happens if we add an S4 modality to Int directly? Things start getting very interesting indeed! It turns out to be best to switch to category theory at this stage. Instead of working with interior operators, lets work with their dual - closure operators (the diamond of S4). Now, the categorical generalisation of a closure operator is what is called a monad. Since Int has as categorical models Cartesian Closed Categories (CCC), what we are effectively trying to do is to add a monad to a CCC. Moreover, since CCC's are equivalent to simply typed lambda calculi, we seem to be doing something sinister to type theory! What we have, in effect, done is to create what is known as the computational lambda calculus. This is a formal framework for reasoning about the equality of programs and was introduced in the following paper:

Computational Lambda Calculus and Monads; Eugenio Moggi

While the computational lambda calculus is, indeed, a rather nifty thing, we seem to have strayed from geometry. Can we get back? We can! One way is to go back to thinking about the box, or interior operator. Categorically, we can see this as a comonad, which preserves some monoidal structure (that of conjunction). We can then interpret this topologically as an "augmented simplicial set". Since simplical sets are a mainstay of topology, we can start thinking geometrically again. This is rather heady, abstract stuff, but you can read all about it here:

On the Geometry of Intuitionistic S4 Proofs; Jean Goubault-Larrecq, Éric Goubault

So, once again, we have derived a huge benefit by asking the question "Why is this result obvious?". Always a good thing to ask!