How to invent intuitionistic logic

(This is an old post I never got around to finishing. It was originally going to have a second half about pointless topology; the interested reader can consult Vickers’ Topology via Logic on this theme.)

Standard presentations of propositional logic treat the Boolean operators “and,” “or,” and “not” as fundamental (e.g. these are the operators axiomatized by Boolean algebras). But from the point of view of category theory, arguably the most fundamental Boolean operator is “implies,” because it gives a collection of propositions the structure of a category, or more precisely a poset. We can endow the set of propositions with a morphism whenever , and no morphisms otherwise. Then the identity morphisms simply reflect the fact that a proposition always implies itself, while composition of morphisms

is a familiar inference rule (hypothetical syllogism). Since it is possible to define “and,” “or,” and “not” in terms of “implies” in the Boolean setting, we might want to see what happens when we start from the perspective that propositional logic ought to be about certain posets and figure out how to recover the familiar operations from propositional logic by thinking about what their universal properties should be.

It turns out that when we do this, we don’t get ordinary propositional logic back in the sense that the posets we end up identifying are not just the Boolean algebras: instead we’ll get Heyting algebras, and the corresponding notion of logic we’ll get is intuitionistic logic.

True, false

Propositional logic should have two special propositions, “true” and “false.” Categorically, we should expect “true” and “false” to have universal properties, and indeed they do: “true” should be implied by everything while “false” should imply everything. In other words, “true” should be a terminal object or top element or greatest element of the poset and “false” should be an initial object or bottom element or least element. We will denote these by and respectively.

Hence the posets we are interested in have both a top and a bottom element; these are the bounded posets.

Example. Starting from any poset , we can adjoin top and bottom elements in the obvious way, and every bounded poset arises in this way for a unique poset (namely the one obtained by removing the top and bottom elements). So this hypothesis is not very restrictive.

And, or

Propositional logic should have a logical “and” operator. Categorically, we again expect a universal property, which is the following: we should have if and only if and . This is precisely the universal property of products, so should be the product or meet or infimum of the two elements . The projection maps reproduce conjunction elimination, another familiar inference rule.

Dually, we need to be able to take the logical “or” of two propositions. The corresponding universal property is that we should have if and only if and . This is precisely the universal property of coproducts, so should be the coproduct or join or supremum of the two elements . The inclusion maps reproduce disjunction introduction. Note in particular that the empty meet is the top element and the empty join is the bottom element.

Hence the posets we are interested in have all finite joins and meets; these are the (bounded) lattices.

Example. Any total order with top and bottom elements is a lattice, where the meet of two elements is their minimum and the join of two elements is their maximum. For example, is such a total order, as is any successor ordinal.

Example. The poset of open subsets of a topological space and the poset of measurable subsets of a measurable space are by definition lattices.

Example. The poset of subobjects of an object in a category is often a lattice. For example, any group has a lattice of subgroups, where the meet is the intersection and the join is the subgroup generated by two subgroups. Similarly, any module has a lattice of submodules, where the meet is the intersection and the join is the sum. In particular, any ring has a lattice of ideals (left, right, or two-sided).

Implies

Propositional logic should have an “internal” notion of implication. In other words, should not only just be true or false but should itself be a proposition. This would allow us to state inference rules like modus ponens (). The corresponding universal property is that if and only if . This is precisely the universal property of exponential objects, which we encountered when talking about the Lawvere fixed point theorem.

For posets, having finite meets is equivalent to having finite limits, and dually having finite joins is equivalent to having finite colimits. A category with finite limits and exponential objects is cartesian closed, and a cartesian closed category with finite coproducts is bicartesian closed. Hence the posets we are interested in are precisely the bicartesian closed posets; these are in turn precisely the Heyting algebras.

Example. Let be a lattice with arbitrary joins such that finite meets distribute over arbitrary joins. Then is cartesian closed and hence a Heyting algebra. This is a consequence of the adjoint functor theorem for posets, and in particular implies that the lattice of open subsets of any topological space is a Heyting algebra. For open sets the implication turns out to be

.

Not

Finally, propositional logic should have a notion of negation. The notion of negation we’ll adopt is that the negation of a proposition asserts that it implies false, so

.

Note that there is no reason for double negation to hold in general. There is also no reason for excluded middle to hold in general. So we’re really in the realm of intuitionistic logic here.

Example. Let be the lattice of open subsets of a topological space as above. Then negation takes the form

.

and can easily fail. For example, let and let . Then , so . Excluded middle fails even more badly: in any topological space, iff is clopen, hence satisfies excluded middle iff is discrete, in which case is a Boolean algebra. is connected iff never satisfies any nontrivial case of excluded middle.

Note, however, that for topological spaces we always have , and in fact in any Heyting algebra we always have

.

To see this, observe that by the universal property this implication holds if and only if , but this follows from modus ponens.