How Do Heyting Algebras Relate To Logic?

Question

My question is, broadly speaking, how are Heyting algebras related to logic ? It would be great if someone could answer this question without being too technical (or point to easy to read literature). I know about category theory, but not much about logic. I know Heyting algebras correspond with the lattices of subobjects in toposes, and I've heard Heyting algebras somehow model intuitionistic logic, but I would really appreciate knowing more about it. I hope my question is not too vague.

Answer 1

As Noah Schweber says, this is a generalization of how Boolean algebras relate to logic, so it would be good to get a handle on that case first. A Boolean algebra $B$ is a set equipped with two elements $\bot, \top$ and operations $\wedge, \vee, \neg$ satisfying the axioms of propositional logic; the intended interpretation is that $B$ is a collection of propositions, $\bot$ is "false," $\top$ is "true," $\wedge$ is "and," $\vee$ is "or," and $\neg$ is "not."

In every Boolean algebra the law of excluded middle $b \vee (\neg b) = 1$ is satisfied. Heyting algebras are, most concretely, a generalization of Boolean algebras in which the law of excluded middle is dropped, and hence which model (propositional) intuitionistic logic.

The definition of a Heyting algebra can be stated and motivated categorically, as done e.g. in my blog post How to invent intuitionistic logic, which explains everything I'm about to explain in more detail. We start by taking the point of view that the most fundamental concept when it comes to propositions is implication, and axiomatize implication as defining a partial order $p \le q$ on the set of propositions (in particular, transitivity corresponds to biconditional introduction: the rule of inference that $p \le q$ and $q \le r$ implies $p \le r$).

Remarkably, every other logical operation now corresponds to requiring that certain universal operations exist with respect to this partial order (in particular, in this framework their properties such as commutativity and associativity are theorems, not axioms):

• $\bot$ is the initial object: this says that $\bot$ is characterized by the property that $\bot \le p$ (false implies everything),
• $\top$ is the terminal object: this says that $\top$ is characterized by the property that $p \le \top$ (everything implies true),
• $p \wedge q$ is the product / meet: this says that $p \wedge q$ is characterized by being universal wrt the property that $p \wedge q \le p$ and $p \wedge q \le q$,
• $p \vee q$ is the coproduct / join: this says that $p \vee q$ is characterized by being universal wrt the property that $p \le (p \vee q)$ and $q \le (p \vee q)$,
• $\neg p$ is the pseudocomplement: this says that $\neg p$ is characterized by being universal wrt the property that $p \wedge (\neg p) = \bot$ (the principle of explosion).

In particular, every Boolean algebra is partially ordered by implication: explicitly, $p \le q$ iff $\neg p \vee q = \top$ (either $p$ is false or $q$ is true), and you can check that all of the above operations exist and have the stated universal properties in a Boolean algebra. So the implication partial order recovers all of the other operations, along with all of their properties.

We can generalize $\neg$ by asking that there exists an object $p \Rightarrow q$ which is universal with respect to the property that $p \wedge (p \Rightarrow q) \le q$; this is (internal) implication, or "relative pseudocomplement," and it recovers negation via taking $\neg p = (p \Rightarrow \bot)$. It can be described in a nice categorical way as follows: asking that $\bot, \top, \wedge, \vee$ exist means asking that propositions form a poset which has all finite limits (/ products / meets) and colimits (/coproducts / joins); these are the (bounded) lattices. To get a Heyting algebra we ask in addition that all implications $p \Rightarrow q$ exist, which is equivalent to asking for all exponential objects. This means that, categorically:

A Heyting algebra is a bicartesian closed poset.

In any Heyting algebra we always have $p \le \neg \neg p$, and we generally do not have equality; if we do, the Heyting algebra must be a Boolean algebra. You can write down lots of interesting examples of Heyting algebras which are not Boolean algebras using the open subsets of most topologies. For more on this you can check out, for example, Vickers' Topology via Logic.