14 Nov 2018

# Discovering Heyting Algebra

We attempt to motivate the structure of a Heyting Algebra by considering ‘inverse problems’.

For example,

• You have a secret number $$x$$ and your friend has a secret number $$y$$, which you've communicated to each other in person.
• You communicate a ‘message’ to each other by adding onto your secret number.
• Hence, if I receive a number $$z$$, then I can undo the addition operation to find the ‘message’ $$m = z - y$$.

What if we decided, for security, to change our protocol from using addition to using minimum. That is, we encode our message $$m$$ as $$z = x ↓ m$$. Since minimum is not invertible, we decide to send our encoded messages with a ‘context’ $$c$$ as a pair $$(z, c)$$. From this pair, a unique number $$m′$$ can be extracted, which is not necessarily the original $$m$$. Read on, and perhaps you'll figure out which messages can be communicated 😉

This exploration demonstrates that relative pseudo-complements

• Are admitted by the usual naturals precisely when infinity is considered a number;
• Are exactly implication for the Booleans;
• Internalises implication for sets;
• Yield the largest complementary subgraph when considering subgraphs.

In some sense, the pseudo-complement is the “best approximate inverse” to forming meets, minima, intersections.

Along the way we develop a number of the theorems describing the relationships between different structural components of Heyting Algebras; most notably the internalisation of much of its own structure.

The article aims to be self-contained, however it may be helpful to look at this lattice cheat sheet (•̀ᴗ•́)و

( Photo by Ludovic Fremondiere on Unsplash )

## 1Meet Semi-Lattices

Recall that an order is nothing more than a type $$Carrier$$ with a relation $$\_⊑\_$$ such that the following list of axioms holds: For any $$x,y,z : Carrier$$,

$\eqn{⊑-reflexive}{x ⊑ x}$

$\eqn{⊑-transitive}{x ⊑ y \landS y ⊑ z \impliesS x ⊑ z}$

$\eqn{⊑-antisymmetric}{x ⊑ y \landS y ⊑ x \impliesS x = y}$

This models notions of containment, inclusion, hierarchy, and approximation.

Recall that a meet is an additional operation $$\_⊓\_$$ specified by $\eqnColour{Meet Characterisation}{ z \;⊑\; x ⊓ y \equivS z ⊑ x \landS z ⊑ y}{green}$

Meets model notions of greatest lower bounds, or infima.

Observe that meets allow us to encode a pair of inclusions as a single inclusion! That is, an external conjunction $$∧$$ is equivalent to an internal meet $$⊓$$.

In computing parlance, think of a top-level ‘method’ that takes and yields data. In many languages, the method itself can be thought of as data! It is this kind of external-internal duality we are alluding to –and is captured nicely by exponential objects in category theory, of which we are considering a special case.

### 1.1Examples

• (ℕ, ≤, ↓) —where ↓ denotes minimum.
• (ℕ, ∣, gcd) –the naturals ordered by divisibility.
• (Sets, ⊆, ∩)
• (𝔹, ⇒, ∧)
• Formulae of a logic ordered by the proves, or syntactic consequence, relationship $$\_⊢\_$$ with syntactic conjunction as meet.
• (Sets, →, ×): Sets with “A atmost B” meaning there is a function $$f : A → B$$, then the Cartesian product can be used as meet.
• This is not strictly a semi-lattice, as defined here, but it is when we consider ‘setoids’.
• Moreover it provides excellent intuition!
• Subgraphs of a given simple graph $$G = (V,E)$$ –which is just a relation $$E$$ on a set of vertices $$V$$.
• The ordering is obtained by subset inclusion, $(V₁, E₁) ⊑ (V₂, E₂) \equivS V₁ ⊆ V₂ \lands E₁ ⊆ E₂$ and so the meet is obtained by intersection, $(V₁, E₁) ⊓ (V₂, E₂) = (V₁ ∩ V₂, E₁ ∩ E₂)$
• However, we cannot define complement in the same fashion, since the resulting relation is not over the resulting vertex set!

Indeed suppose we define $$∼ (V′, E′) \;:=\; (V - V′, E - E′)$$, then the discrete graph $$(V, ø)$$ has complement $$(ø, E)$$ which is a ‘graph’ with many edges $$E$$ but no vertices! —Provided $$(V,E)$$ has edges.

However, the edges can be relativised to the vertices to produce the pseudo-complement.

### 1.2The Principle of Indirect Equality

It is not clear how $$\ref{Meet Characterisation}$$ can be used to prove properties about meet.

The laws \ref{⊑-antisymmetric} and \ref{⊑-reflexive} can be fused together into one law: $\eqnColour{Indirect Equality}{ x = y \equivS \left(∀ z \;•\quad ⊑\; z ⊑ x \equivs z ⊑ y\right)}{green}$

That is, for all practical purposes, $$x = y$$ precisely when they have the same sub-parts!

Using this, we can prove that meet is idempotent $$x ⊓ x = x$$, symmetric $$x ⊓ y = y ⊓ x$$, associative $$x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ z$$, and monotonic: $$a ⊑ b \landS c ⊑ d \impliesS a ⊓ c \sqleqS b ⊓ c$$.

Below we use this principle in a number of places, for example \ref{Distributivity of → over ⊓}.

## 2Relative Pseudo-complements

The relative pseudo-complement of $$a$$ wrt $$b$$, $$(a ⟶ b)$$, is “the largest element $$x$$ that ensures modus ponens”, i.e., “the largest element $$x$$ whose meet with $$a$$ is contained in $$b$$”:

$\eqnColour{Relative Pseudo-Complement Characterisation}{\hspace{-5em} a ⊓ x \;⊑\; b \equivS x \;⊑\; (a → b)}{green}$

This is also sometimes denoted $$a ➩ b$$ or $$a \backslash b$$.

In five of the above settings this becomes,

• $$m ↓ x ≤ n \equivS x ≤ (m → n)$$

Not at all clear what to do so looking for a counterexample shows that pseduocomplements cannot exist for the naturals otherwise selecting $$m ≔ n$$ yields:

\begin{calc} ∀ x \;•\quad n ↓ x \;≤\; n \equivS x \;≤\; (n → n) \step{ Weakening: The minimum is at least both its arguments } ∀ x \;•\quad \mathsf{true} \equivS x \;≤\; (n → n) \step{ Identity of ≡ } ∀ x \;•\quad x \;≤\; (n → n) \step{ Definition of Infinity } (n → n) \;=\; +∞ \end{calc}

Thus the existence of psquedo-complements implies the existence of a top element “$$(n ⟶ n) = +∞$$”!

Okay, no problem: Let's consider 𝒩, the set of natural numbers along with a new maximum element “+∞”; then we can define a relative pseudo-complement. $\eqn{Definition of → for 𝒩}{m → n \quad=\quad \mathsf{if}\; m > n \;\mathsf{then}\; n \;\mathsf{else}\; +∞ \;\mathsf{fi}}$ We now have a way to approximate an inverse to minima, which is in general not invertible.

–This definition works for any linear order with a top element—

• $$p ∧ x ⇒ q \equivS x ⇒ (p → q)$$

Starting with the right side,

\begin{calc} x \impliesS (p → q) \step{ Characterisation of pseudo-complement } p ∧ x \impliesS q \step{ Symmetry of ∧ } x ∧ p \impliesS q \step{ Shunting } x \impliesS (p ⇒ q) \end{calc}

Hence, by indirect equality, $$p → q \;=\; p ⇒ q \;=\; ¬ p ∨ q$$.

• $$(A ∩ X) \;⊆\; B \equivS X \;⊆\; (A → B)$$

Where we can similarly verify $$(A → B) \;\;=\;\; ∼ A ∪ B$$.

It is interesting to note that $$x ∈ (A → B) \equivS x ∈ A \impliess x ∈ B$$.

• $$G ⊓ X \;⊑\; G′ \equivS X \;⊑\; (G → G′)$$

We disclosed earlier that subgraph difference did not yield valid subgraphs, but if we relativised the resulting edge relationship to only consider the resulting vertex set, then we do have a subgraph.

That is, subgraphs admit relative pseduo-complements, by $$(V₁, E₁) → (V₂, E₂) \equivS (V₁ - V₂, (E₁ - E₂) ∩ (V₃ × V₃))$$ where $$V₃ = V₁ - V₂$$.

The result of $$G₁ → G₂$$ is the largest subgraph of $$G₁$$ that does not overlap with $$G₂$$.

• $$(A × B → C) \equivS A → (B → C)$$

In the setting of functions, this says that a function taking a pair of inputs can be considered as a function that takes one input, of type $$A$$, then yields another function that takes the second input. That is, the two inputs no longer need to be provided at the same time. This is known as currying.

• $$P, Q ⊢ R \equivS P ⊢ (Q → R)$$

In the logical formulae setting, the characterisation is known as the deduction theorem and allows us to ‘suppose’ an antecedent in the process of a proof.

In the above we have witnessed that the usual naturals admit pseudo-complements precisely when infinity is considered a number, that it is exactly implication for the Booleans, that it internalises implication for sets, and for subgraphs it is encodes the largest complementary subgraph.

In some sense, the pseudo-complement is the “best approximate inverse” to forming minima.

We leave the remaining example as an exercise 😉

## 3Theorems — Generalising Observations from the Examples

Recall the \ref{Relative Pseudo-Complement Characterisation} says $a ⊓ x \;⊑\; b \equivS x \;⊑\; (a → b)$

We readily obtain some results by making parts of the characterisation true. E.g., making the left/right part true by instantiating the variables.

For example, taking $$x ≔ (a → b)$$ yields $\eqn{Modus Ponens}{a ⊓ (a → b) \quad⊑\quad b}$ Exercise: Prove this directly!

• In the Boolean setting, this reads “if $$a$$ is true and $$a$$ implies $$b$$, then $$b$$ is true”.
• In the functional setting, this reads “if $$f : A → B$$ and we have an element $$a : A$$, then we have an element $$f(a) \, : \, B$$”. In this setting, this operation is known as ‘evaluation’, or function application.

Using the principle of indirect equality, we can strengthen this into an equality and also obtain a close variant. $\eqn{Strong Modus Ponens}{a ⊓ (a → b) \quad=\quad a ⊓ b}$

$\eqn{Absorption}{b ⊓ (a → b) \quad=\quad b}$

\ref{Modus Ponens} suggest an order preservation property:

Hence we have derived the following consequent weakening rule, $\eqn{Monotonicity₂}{a → x \quad⊑\quad a → y \qquad\Leftarrow\qquad x \;⊑\; y}$

An immediate sequel is, $\eqn{Weakening₂}{a → (x ⊓ y) \quad⊑\quad a → y}$

Here are a few more properties for you to get familiar with this, the first three are immediate instantiation of the characterisation, while the fourth one may require using monotonicity properties of meet, and the final one uses indirect equality.

$\eqn{Top Element}{x \quad⊑\quad a → a}$

$\eqn{Strengthening}{b \quad⊑\quad a → b}$

$\eqn{UnCurrying}{x \quad⊑\quad a → a ⊓ x}$

$\eqn{Weakening}{x \quad⊑\quad (a ⊓ b) → b}$

$\eqn{Antitonicity₁}{a → x \quad⊑\quad b → x \qquad\Leftarrow\qquad b \;⊑\; a}$

$\eqn{Self-Sub-Distributive}{a → (b → c) \sqleqS (a → b) → (a → c)}$

Observe that, in the functional case, \ref{UnCurrying} says we have a function $X → (A → (A × X)) \;\;:\;\; x \mapsto (a \mapsto (a, x))$

## 4→ Furnishes ⊓

Recall \ref{Top Element} said that we have a greatest element in the order. Suppose our universe, $$Carrier$$, is non-empty and has some element $$c₀$$. Then we may define $$⊤ = (c₀ → c₀)$$. This element is in-fact invariant over $$c₀$$:

$\eqn{Top Element Invariance}{ ∀ x \;•\quad ⊤ \quad=\quad (x → x) }$ The proof is simply an appeal to \ref{⊑-antisymmetric} then \ref{Top Element} twice.

From this, we obtain two immediate properties about meets.

$\eqn{Identity of ⊓}{ x ⊓ ⊤ \quad=\quad x }$

$\eqn{Shunting}{x \;⊑\; a → (b → c) \equivS x \;⊑\; (a ⊓ b) → c}$

Along with two properties about top element.

$\eqn{Right Zero of →}{ x → ⊤ \quad=\quad ⊤ }$

$\eqn{Left Identity of →}{ ⊤ → x \quad=\quad x }$

Notice that \ref{Right Zero of →} internalises what it means to be a \ref{Top Element}; namely $$∀ x \;•\; x ≤ ⊤$$.

A bit more interestingly, we can fuse a meet with a pseudo-complement:

$\eqn{Sub-mutual Associtivity of ⊓ and →}{\hspace{-3em}x ⊓ (a → b) \sqleqS (x ⊓ a) → b}$

The converse of this statement is not true in general. In particular, in the presence of bottoms, the converse, $$(x ⊓ a) → b \;\;⊑\;\; x ⊓ (a → b)$$, implies that there is only one possible value: ⊥!

Exercise: Show that the converse statement implies $$⊥ = ⊤$$ then from this conclude that $$x = ⊥$$, for all $$x$$.

## 5Internalising ⊑ and ⊓

We have seen how relative pseudo-complements allowed us to reflect external characterisations such as \ref{Top Element} that use logical connectives into internal forms such as \ref{Right Zero of →} which only uses the symbols of the language, namely →, ⊓, ⊤.

Even the order, which takes two elements and yields a Boolean, can be internalised: $\eqn{Internalising}{a ⊑ b \equivS (a → b) = ⊤}$

Notice the striking resemblance to the \ref{Definition of → for 𝒩}!

\ref{Meet Characterisation} can also be internalised:

\begin{calc} x \sqleqS (a → c) \;⊓\; (a → b) \step{ \ref{Meet Characterisation} } x ⊑ (a → c) \landS x ⊑ (a → b) \step{ \ref{Relative Pseudo-Complement Characterisation} } a ⊓ x ⊑ c \landS a ⊓ x ⊑ b \step{ \ref{Meet Characterisation} } a ⊓ x \sqleqS c ⊓ b \step{ \ref{Relative Pseudo-Complement Characterisation} } x \sqleqS a → (c ⊓ b) \end{calc}

Hence, by the principle of \ref{Indirect Equality}, we have $\eqn{Distributivity of → over ⊓}{ a → (c ⊓ b) \quad=\quad (a → c) \;⊓\; (a → b) }$

## 6Flipping the Inclusions Around

Recall \ref{Meet Characterisation} says $z \;⊑\; x ⊓ y \equivS z ⊑ x \landS z ⊑ y$ If we now mirror ‘⊑’ with ‘⊒’ we obtain –after renaming ⊓ with ⊔– $z \;⊒\; x ⊔ y \equivS z ⊒ x \landS z ⊒ y$ That is, we obtain upper bounds! $\eqnColour{Join Characterisation}{ x ⊔ y \;⊑\; z \equivS x ⊑ z \landS y ⊑ z}{green}$

Moreover, using →, it can be shown that joins and meets distribute over each other.

$\eqn{Distributivity₁}{a \;⊔\; (b ⊓ c) \quad=\quad (a ⊔ b) \;⊓\; (a ⊔ c)}$ $\eqn{Distributivity₂}{a \;⊓\; (b ⊔ c) \quad=\quad (a ⊓ b) \;⊔\; (a ⊓ c)}$

## 7Almost True Complements

Can we obtain the usual De Morgan's law?

Suppose we have a least element $$⊥ : Carrier$$, i.e., for any $$x$$, $\eqn{Bottom Element}{ ⊥ \sqleqs x}$

For usual ℕ, 𝔹, sets, and graphs this amounts to 0, $$\mathsf{false}$$, $$\emptyset$$, and the empty graph with no nodes nor any edges, respectively.

Unsurprising this can also be internalised! $\eqn{ex falso quod libet}{⊥ → a \quad=\quad ⊤}$

Moreover we can now define an operation $$¬\_$$ as follows, $\eqn{Pseudo-Complement Definition}{ ¬ x \quad=\quad (x → ⊥) }$

A complement of an element $$x$$ is an element $$y$$ that is disjoint from $$x$$ and together their join is the top element.

A pseudo-complement generalises this idea by discarding the second half of that conjunction; i.e., instead requiring a greatest element $$y$$ disjoint from $$x$$.

Indeed this is the case here,

\begin{calc} x \;⊓\; ¬ x \quad=\quad ⊥ \step{ \ref{⊑-antisymmetric} } (x \;⊓\; ¬ x) \sqleqs ⊥ \landS ⊥ \sqleqs (x \;⊓\; ¬ x) \step{ \ref{Bottom Element} } x \;⊓\; ¬ x \sqleqS ⊥ \step{ \ref{Modus Ponens} } \mathsf{true} \end{calc}

We now have the linguistic prerequisites to actually express De Morgan's laws. $\eqn{Constructive De Morgan}{¬(x \;⊔\; y) \quad=\quad ¬ x \;⊓\; ¬ y}$

The other form $$¬(x ⊓ y) \;=\; ¬ x ⊔ ¬ y$$ however is not true in general. Likewise neither are double negation, $$¬¬x \;=\; x$$, nor the law of the the excluded middle $$x \;⊔\; ¬ x \;=\; ⊤$$.

Indeed for 𝒩, the natural numbers extended with +∞, the law of the exluded middle is falsified as follows:

\begin{calc} 3 ↑ ¬ 3 \step{ \ref{Pseudo-Complement Definition} } 3 ↑ (3 → 0) \step{ \ref{Definition of → for 𝒩} } 3 ↑ 0 \step{ Maximum } 3 \end{calc}

Likewise double negation is falsified by $$¬ ¬ 3 \;=\; 0$$.

Exercise: Find an example to falsify the other De Morgan's law.

Having ⊓, ⊔, ⊥, ⊤, → together constitutes a Heyting Algebra.

## 8So long and thanks for the fish

It took a while, but we've more or less shimmied our way to the structure needed for Heyting Algebras.