Notes on Heyting Algebras

Heyting-algebras.md

Heyting Algebras

A Heyting algebra is a bicartesian closed poset. I.e.,

• It has a greatest element 1 (top, true)
• It has a least element 0 (bottom, false)
• It has all meets (intersections, products, logical "and")
• It has all joins (unions, coproducts, sums, logical "or")
• It has all horseshoes (internalized implications, exponentials, the material conditional)

Notation:

• To write "less than or equal to," I will just write <. I don't mean "strictly less than." I mean "less than or equal to."
• To write a horeshoe (material conditional, I will write =>.

Interpret x < y as x entails/meta-implies y, i.e., we interpret the < as an arrow in a skeletal category.

Heyting implication

I will call a material implication a "horseshoe," to try and keep away from using the term "implication," which can be ambiguous between meta-application, object-language implication, and an internalized implication object.

What is the horseshoe in a Heyting algebra? Given p < q, there is some point in the lattice that is an internal representation of the meta-implication. As a name for this point, we write (p => q). It's like how in the category of Set, an exponential is an "internal homset," i.e., it's the set of arrows between two objects, but since it's a set, it's also an object in the same category. Likewise, (p => q) is a point in the lattice too, even though it encodes the arrow between p and q.

How do we know which element (p => q) is? For that, we need to investigate the properties of this element.

The basic idea behind a horeshoe (material implication) is modus ponens: given (p => q) and p, we can metainfer q. Taking < as our symbol for meta-implies and /\ as our symbol for meta-and, we can write that like this:

(p => q) /\ p < q

In the lattice, this means that the meet of (p => q) (whichever element it is) and p must be below q in the lattice.

This isn't enough to uniquely determine which point in the lattice (p => q) actually is. There might be more than one point c which satisfies:

c /\ p < q

What we want is the highest such c in the lattice that satisfies c /\ p < q. In other words, any candidate c must be lower than the actual horseshoe element (p => q). Hence, we can say:

c < (p => q)

As a side note, notice that this puts us in an "if and only if" situation here:

c /\ p < q iff c < (p => q)

Why do all the candidates have to be lower than the real (p => q) candidate? Because the universal property says that every candidate will have a unique arrow to the real (p => q) that makes the evaluation arrow commute. In lattices, we have only one arrow between every object, so this just means we need one arrow from the candidate to the real (p => q). Well, which element out of a set of candidates is the one that all the others have one arrow to but it has no arrow to them? It's the highest one. Hence, the real (p => q) is going to be the highest element for which the modus ponens rule holds.

Examples

Take this simple lattice:

     1
   /   \
  d     e
   \   /
     0

1. We can see that 0 < 0 in the lattice, so there should be an element (0 => 0) sowhere in this lattice. Which element is it? First, find every candidate c which is such that c /\ 0 < 0. There are four candidates: 0, d, e, and 1 (because the meet of 0 and any other element is 0). Now, which of them is the greatest? It is 1. So 1 is (0 => 0).

2. We can see that 0 < d in the lattice, so there should be an element (0 => d) somewhere in this lattice. Which element is it? First, find every candidate c which is such that c /\ 0 < d. There are four candidates again, for the same reason. And again, which of them is the greatest? It is 1, so 1 is (0 => d).

3. We can see that 0 < 1 in the lattice, so there should be an element (0 => 1) somewhere in this lattice. Which element is it? First, find every candidate element c which is such that c /\ 0 < 1. There are four candidates again, for the same reason as before. And which is the greatest? It is 1, so 1 is (0 => 1).

4. We can see that d < 1 in the lattice, so there should be an element (d < 1) somewhere in this lattice. Which element is it? First, find every candidate c which is such that c /\ d < 1. There are two candidates: d and 1. Which of them is the greatest? It is 1 again.

5. What about (d => e)? Is there an element that represents this? It might be tempting to think no, because it is not true that d < e. In fact d and e are not comparable in this lattice, so can there be an implication between them at all? Well, if there is, then it would need to be a c such that c /\ d < e. Is there any such element? There are two: 0 and e (since the meet of d and 0 is 0, and the meet of d and e is 0, and 0 is lower than e). So, e is the (d => e) element.

6. What about (d => 0)? Is there an element that represents this? If there is, it would need to be a c such that c /\ d < 0. There are two candidates, namely 0 and e. The highest such element is e, so that's the answer.

Consider this lattice:

 1
 |
1/2
 |
 0

1. What is (0 => 0)? Which cs satisfy c /\ 0 < 0? It's {0, 1/2, 1}. The greatest is 1.
2. What is (0 => 1/2)? Which cs satisfy c /\ 0 < 1/2? It's the same.
3. What is (0 => 1)? Ditto.
4. What is (1/2 => 1/2)? Which cs satisfy c /\ 1/2 < 1/2? It's {0, 1/2, 1}. The greatest is 1.
5. What is (1/2 => 1)? Which cs satisfy c /\ 1/2 < 1? It's {0, 1/2, 1}. The greatest is 1.
6. What is (1 => 1)? Which cs satisfy c /\ 1 < 1? It's {0, 1/2, 1}. The greatest is 1.
7. What is (1/2 => 0)? Which cs satisfy c /\ 1/2 < 0? It's {0}. So it's 0.
8. What is (1 => 1/2)? Which cs satisfy c /\ 1 < 1/2? It's {0, 1/2}. The greatest is 1/2.
9. What is (1 => 0)? Which cs satisfy c /\ 1 < 0)? It's {0}. So it's 0.

In this case, it's a totally ordered set, and I observe that: if p < q, then (p => q) is 1. Otherwise, (p => q) is q.

Calculating the horseshoe?

Heyting algebras are bicartesian closed posets, and that means they have all exponentials. In other words, there is a horeshoe for each pair of points in the lattice.

Given any two points in the lattice, is there a rule for calculating which element is the horseshoe? I think there is, if it's a totally ordered poset.

Suppose that p < q is true in the lattice. We know that the modus ponens inequality must be true: (p => q) /\ p < q. Which element c can meet with p to preserve this? If c is below p, then it satisfies the inequality, since the meet with c and p will be at least as low as c, and p is lower than q too, so by transitivity c < p < q. If c is p, then it satisfies the inequality too, because p /\ p is p, and we know that p < q. If c is above p, the the meet of c /\ p will either be p (if they're in the same path), or lower (if they're not in the same path and we need to drop lower to find a point where they meet). Hence, if c is above p, it will still satisfy the modus ponens inequality, because the meet of it and p will end up below q anyway. We can see from this that, if p < q, then any c will satisfy the modus ponens inequality! But the real horeshoe is the greatest one, so what's the greatest element of the whole lattice? It's 1. Hence, if p < q in the lattice, then (p => q) is 1.

Now suppose that it's not the case that p < q. Hence, p is strictly higher than q (remember that I write < to mean "less than or equal to"). What element is (p => q). It must satisfy the modus ponens inequality c /\ p < q. There are two cases: either c is lower than p, or c is higher than p.

Case 1: suppose c is p or lower. If it's p, well then it's too high to satisfy the modus ponens inequality (remember that p is strictly higher than q). So, c has to drop down until it's at least as low as q. If it's q or lower, then the meet of c and p will be that element of q or lower, and hence any element from q and lower will satisfy the inequality. But we need to take the highest such element, and that's q. So, if c is p or lower, then q will be (p => q).

Case 2: suppose c is strictly higher than p. Well, then it's too high to satisfy the modus ponens inequality. So c has to drop down until it's at least as low as q. Again then, the set of candidates are q and lower. To get the real horshoe, we take the greatest of the candidates, which is q. Hence, if c is p or higher, then q again is (p => q).

We can conclude from this that if it's not the case that p < q, then (p => q) is q.

That gives us the rule: if p < q then (p => q) is 1, otherwise (p => q) is q.