# 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 )

## 1 Meet 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.1 Examples

- (ℕ, ≤, ↓) —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.2 The 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 ⊓}.

## 2 Relative 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 😉

## 3 Theorems — 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:

\begin{calc} a → x \quad⊑\quad a → y \step{ \ref{Relative Pseudo-Complement Characterisation} } a ⊓ (a → x) \quad⊑\quad y \stepWith{\Leftarrow}{ \ref{⊑-transitive} } a ⊓ (a → x) \quad⊑\quad x \landS x \quad⊑\quad y \step{ \ref{Modus Ponens} and Identity of ∧ } x \quad⊑\quad y \end{calc}
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\).

## 5 Internalising ⊑ 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) }\]

## 6 Flipping 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)}\]

## 7 Almost *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.

## 8 So 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.

Hope you had fun!

**Generated by Emacs and Org-mode (•̀ᴗ•́)و**