#+TITLE: Discovering Heyting Algebra #+DATE: <2018-11-14 19:29> #+AUTHOR: Musa Al-hassy #+EMAIL: alhassy@gmail.com * Abstract :ignore: :PROPERTIES:... We attempt to motivate the structure of a Heyting Algebra by considering ‘inverse problems’. For example, + You have a secret number and your friend has a secret number 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 then I can undo the addition operation to find the ‘message’ What if we decided, for security, to change our protocol from using addition to using minimum. That is, we encode our message as Since minimum is not invertible, we decide to send our encoded messages with a ‘context’ as a pair From this pair, a unique number can be extracted, which is not necessarily the original Read on, and perhaps you'll figure out which messages can be communicated 😉 # For example, we wrote our message on a piece of paper and placed it on a cafe bulletin board --a context! 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. # + Generalise the deduction theorem. 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 (•̀ᴗ•́)و * Photograph Credit :ignore: :PROPERTIES:... ( Photo by Ludovic Fremondiere on Unsplash ) # "Download free do whatever you want high-resolution photos from Unsplash." * Meet Semi-Lattices :PROPERTIES:... Recall that an order is nothing more than a type with a relation such that the following list of axioms holds: For any This models notions of containment, inclusion, hierarchy, and approximation. Recall that a meet is an additional operation specified by 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. ** Examples :PROPERTIES:... + (ℕ, ≤, ↓) ---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 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 --which is just a relation on a set of vertices - The ordering is obtained by subset inclusion, and so the meet is obtained by intersection, # Likewise joins are given by unions. - However, we cannot define complement in the same fashion, since the resulting relation is not over the resulting vertex set! Indeed suppose we define then the discrete graph has complement which is a ‘graph’ with many edges but no vertices! ---Provided has edges. However, the edges can be relativised to the vertices to produce the pseudo-complement. # Every interior algebra provides a Heyting algebra in the form of its lattice of open elements. Every Heyting algebra is of this form as a Heyting algebra can be completed to a Boolean algebra by taking its free Boolean extension as a bounded distributive lattice and then treating it as a generalized topology in this Boolean algebra. ** The Principle of Indirect Equality :PROPERTIES:... It is not clear how can be used to prove properties about meet. # Recall it says, for any $x, y, z$, # \[ z \;⊑\; x ⊓ y \equivS z ⊑ x \landS z ⊑ y \] The laws \ref{⊑-antisymmetric} and \ref{⊑-reflexive} can be fused together into one law: That is, for all practical purposes,precisely when they have the same sub-parts! Using this, we can prove that meet is idempotent symmetric associative and monotonic: Below we use this principle in a number of places, for example \ref{Distributivity of → over ⊓}. * Relative Pseudo-complements :PROPERTIES:... The relative pseudo-complement ofwrt $b$, is “the largest elementthat ensures modus ponens”, i.e., “the largest elementwhose meet withis contained in: This is also sometimes denoted or In five of the above settings this becomes, + Not at all clear what to do so looking for a counterexample shows that pseduocomplements cannot exist for the naturals otherwise selecting yields: # $n ↓ x ≤ n ≡ x ≤ (n → n)$ i.e., $true ≡ x ≤ (n → n)$ # and so existence of psquedo-complements implies the existence of a top element “$(n ⟶ n) = +∞$”! # Question: Why does this pass `quickCheck $ \m -> \n -> \x -> (m `min` x <= n) = (x <= n)`? Thus the existence of psquedo-complements implies the existence of a top element ! 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. 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--- + Starting with the right side, Hence, by indirect equality, + Where we can similarly verify It is interesting to note that + 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 where The result ofis the largest subgraph ofthat does not overlap with + 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 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. + 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 😉 * Theorems --- Generalising Observations from the Examples :PROPERTIES:... Recall the \ref{Relative Pseudo-Complement Characterisation} says 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 yields Exercise: Prove this directly! + In the Boolean setting, this reads “if is true and implies then is true”. + In the functional setting, this reads “if and we have an element then we have an element . 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. :Proof:... :Proof:... # $a ⊓ x \;⊑\; b \equivS x \;⊑\; (a → b)$ \ref{Modus Ponens} suggest an order preservation property: Hence we have derived the following consequent weakening rule, An immediate sequel is, 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. # Taking b ≔ a # Take x ≔ b # Take b ≔ a ⊓ x # Take a ≔ a ⊓ b :Proof:... :Proof:... Observe that, in the functional case, \ref{UnCurrying} says we have a function * → Furnishes ⊓ :PROPERTIES:... Recall \ref{Top Element} said that we have a greatest element in the order. Suppose our universe, is non-empty and has some element Then we may define This element is in-fact invariant over The proof is simply an appeal to \ref{⊑-antisymmetric} then \ref{Top Element} twice. From this, we obtain two immediate properties about meets. :Proof:... :Proof:... Along with two properties about top element. :Proof:... # The next one can be easily proven using indirect equality. :Proof:... Notice that \ref{Right Zero of →} internalises what it means to be a \ref{Top Element}; namely A bit more interestingly, we can fuse a meet with a pseudo-complement: # The next one needs antitonicity in the first argument of `→'! # “Lower adjoint after upper adjoint is contained in the reversal” :Proof:... The converse of this statement is not true in general. In particular, in the presence of bottoms, the converse, implies that there is only one possible value: ⊥! Exercise: Show that the converse statement implies then from this conclude that for all :Proof:... # Every element x with the property x* = 0 (or equivalently, x** = 1) is called dense. * Internalising ⊑ and ⊓ :PROPERTIES:... 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: :Proof:... Notice the striking resemblance to the \ref{Definition of → for 𝒩}! \ref{Meet Characterisation} can also be internalised: Hence, by the principle of \ref{Indirect Equality}, we have * Flipping the Inclusions Around :PROPERTIES:... # -- Adding -⊔- Recall \ref{Meet Characterisation} says If we now mirror ‘⊑’ with ‘⊒’ we obtain --after renaming ⊓ with ⊔-- That is, we obtain upper bounds! # (x → z) ⊓ (y → z) ⊑ (x ⊔ y) → z Moreover, using →, it can be shown that joins and meets distribute over each other. :Proof:... * Almost True Complements :PROPERTIES:... # -- Adding ⊥ Can we obtain the usual De Morgan's law? Suppose we have a least element i.e., for any For usual ℕ, 𝔹, sets, and graphs this amounts to 0, and the empty graph with no nodes nor any edges, respectively. Unsurprising this can also be internalised! :Proof:... Moreover we can now define an operation as follows, A complement of an element is an element that is disjoint from 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 disjoint from Indeed this is the case here, We now have the linguistic prerequisites to actually express De Morgan's laws. The other form however is not true in general. Likewise neither are double negation, nor the law of the the excluded middle Indeed for 𝒩, the natural numbers extended with +∞, the law of the exluded middle is falsified as follows: Likewise double negation is falsified by Exercise: Find an example to falsify the other De Morgan's law. Having ⊓, ⊔, ⊥, ⊤, → together constitutes a Heyting Algebra. ** COMMENT Old stuff :PROPERTIES:... Let's close by showing that relative pseudo-complementsare the largest subparts ofdisjoint from We can say two elements are disjoint when their commonality is the least element; i.e., when With this setup, our final claim can be phrased as Let's prove it! # Counter-example to: a → b = a ⊓ (b → ⊥) # = p ⇒ q ≡ p ∧ ¬ q # = p ∧ q ≡ p ≡ p ∧ ¬ q # = p ∧ (q ≡ ¬ q ≡ true) # = p ∧ false # = false Indeed, it seems more often that: a → b = ¬ a ⊔ b Provided ¬ is a true complement. ¬ a ⊔ b ⊑ a → b ≡ a ⊓ (¬ a ⊔ b) ⊑ b ≡ (a ⊓ ¬ a) ⊔ (a ⊓ b) ⊑ b ≡ ⊥ ⊔ (a ⊓ b) ⊑ b -- since ¬ is a real complement. ≡ a ⊓ b ⊑ b ≡ true And the converse? * So long and thanks for the fish :PROPERTIES:... It took a while, but we've more or less shimmied our way to the structure needed for Heyting Algebras. Hope you had fun!