Discovering Heyting Algebra

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.

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 😉

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))\]

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\).

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

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

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.

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

Hope you had fun!