How to invent intuitionistic logic

December 10, 2013 by Qiaochu Yuan

(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 $p \to q$ whenever $p \Rightarrow q$ , and no morphisms otherwise. Then the identity morphisms $\text{id}_p : p \to p$ simply reflect the fact that a proposition always implies itself, while composition of morphisms

$\displaystyle (p \Rightarrow q) \wedge (q \Rightarrow r) \to (p \Rightarrow r)$

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 $\top$ and $\bot$ 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 $P$ , we can adjoin top and bottom elements in the obvious way, and every bounded poset arises in this way for a unique poset $P$ (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 $p \Rightarrow (q \wedge r)$ if and only if $p \Rightarrow q$ and $p \Rightarrow r$ . This is precisely the universal property of products, so $q \wedge r$ should be the product or meet or infimum of the two elements $q, r$ . The projection maps $q \wedge r \to q, q \wedge r \to r$ 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 $(p \vee q) \Rightarrow r$ if and only if $p \Rightarrow r$ and $q \Rightarrow r$ . This is precisely the universal property of coproducts, so $p \vee q$ should be the coproduct or join or supremum of the two elements $p, q$ . The inclusion maps $p \to p \vee q, q \to p \vee q$ 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, $\mathbb{R} \sqcup \{ -\infty, +\infty \}$ 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 $G$ has a lattice of subgroups, where the meet is the intersection and the join is the subgroup generated by two subgroups. Similarly, any module $M$ has a lattice of submodules, where the meet is the intersection and the join is the sum. In particular, any ring $R$ has a lattice of ideals (left, right, or two-sided).

Implies

Propositional logic should have an “internal” notion of implication. In other words, $p \Rightarrow q$ 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 ( $p \wedge (p \Rightarrow q) \to q$ ). The corresponding universal property is that $p \Rightarrow (q \Rightarrow r)$ if and only if $(p \wedge q) \Rightarrow r$ . 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 $L$ be a lattice with arbitrary joins such that finite meets distribute over arbitrary joins. Then $L$ 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 $O(X)$ of open subsets of any topological space $X$ is a Heyting algebra. For open sets $U, V$ the implication $U \Rightarrow V$ turns out to be

$\displaystyle (U \Rightarrow V) = \text{int}(U^c \cup V)$ .

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

$\displaystyle \neg p = (p \Rightarrow \bot)$ .

Note that there is no reason for double negation $\neg (\neg p) = p$ to hold in general. There is also no reason for excluded middle $p \vee (\neg p)$ to hold in general. So we’re really in the realm of intuitionistic logic here.

Example. Let $L = O(X)$ be the lattice of open subsets of a topological space as above. Then negation takes the form

$\displaystyle \neg U = \text{int}(U^c)$ .

and $\neg (\neg U) = U$ can easily fail. For example, let $X = \mathbb{R}$ and let $U = \mathbb{R} \setminus \mathbb{Z}$ . Then $\neg U = \emptyset$ , so $\neg (\neg U) = \mathbb{R}$ . Excluded middle fails even more badly: in any topological space, $U \cup (\neg U) = X$ iff $U$ is clopen, hence $O(X)$ satisfies excluded middle iff $X$ is discrete, in which case $O(X) = 2^X$ is a Boolean algebra. $X$ is connected iff $O(X)$ never satisfies any nontrivial case of excluded middle.

Note, however, that for topological spaces we always have $U \subseteq \neg (\neg U)$ , and in fact in any Heyting algebra we always have

$p \Rightarrow \neg (\neg p)$ .

To see this, observe that by the universal property this implication holds if and only if $(p \wedge (p \Rightarrow \bot)) \Rightarrow \bot$ , but this follows from modus ponens.

3 Responses

on February 21, 2014 at 4:35 am | Reply Owen Biesel

A fun consequence of $p \Rightarrow \neg(\neg p)$ is that $\neg p \Leftrightarrow \neg(\neg(\neg p))$ ; the two implications are the case $\neg p$ in the original statement and the contrapositive of the original statement for $p$ .

As a result, those elements of a Heyting algebra which are negations, called regular elements, are exactly those elements for which double negation holds. The regular elements form a Boolean algebra with the same $\top, \bot, \wedge, \Rightarrow$ , and $\neg$ , but may have a different $\vee$. For example, the “regular” (in this sense) open subsets of a topological space are those which are the interiors of their closures, and this property is preserved under intersection. However, the “join” of the open intervals $(0,1)$ and $(1,2)$ in this Boolean algebra is $(0,2)$ , not $(0,1)\cup(1,2)$ .
on January 6, 2014 at 7:33 am | Reply Boolean Algebra |

[…] How to invent intuitionistic logic | Annoying Precision https://qchu.wordpress.com/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 … 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, mathbb{R} sqcup { -infty, +infty is such a total order, as is … […]
on December 15, 2013 at 7:32 am | Reply Boolean Algebra |

[…] How to invent intuitionistic logic | Annoying Precision https://qchu.wordpress.com/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, … […]

Comments RSS

	CG on GILA V: The Polya enumeration…
	rajeshd007 on Gradient descent
	Robert on Gradient descent
	Qiaochu Yuan on Gradient descent
	Kram Einsnulldreizwe… on Gradient descent

Annoying Precision

"A good stock of examples, as large as possible, is indispensable for a thorough understanding of any concept, and when I want to learn something new, I make it my first job to build one." – Paul Halmos