Logic and Category - Or Planar Heyting Algebras for Children

Eduardo Ochs

Federal Fluminense University, Rio das Ostras, Brazil

One way to explain intuitionistic logic to a non-logician is this. The usual truth-values are just 0 and 1, and we will change that by decreeing that the new truth-values will be certain diagrams with several 0s and 1s. We choose a subset D of ℕ², for example _•^•_•, and we say that a modal truth-value on D is a way of assigning 0s and 1s to the points of D. A modal truth value is unstable when it has a 1 immediately above a 0, for example ₁¹₀ is unstable, and an intuitionistic truth-value on D is a stable modal truth-value on D. Now that we have defined our (intuitionistic) truth-values we explain to our non-logician friend how to interpret ⊤, ⊥, ∧, ∨, → on them, and we show that if P = ₁⁰₁ then P ≠ ¬¬P = ₁¹₁, and some other classical theorems also do not hold. We then explain some logical axioms and rules that do hold in this system, define intuitionistic propositional logic from them, show how this particular case based on D generalizes, present the standard terminology, and so on.

When we do this we are using several tricks – finding an insightful particular case, doing things in the particular and in the general cases in parallel using diagrams with the same shapes, lifting proofs from the particular case to the general one –, and this dydactical method can be defined precisely. In the terminology of [Ochs2013] this logic on subsets of ℕ² and DAGs on them (ZSets and ZDAGs) is an archetypal model for intuitionistic propositional logic (“IPL”). If we abbreviate “explaining and formalizing (something) via an archetypal model” as “(that something) for children”, then the contents of the tutorial become easy to state.

Heyting Algebras for children. When a ZDAG D doesn't have three independent points, then the open sets of (D, O(D)) are in bijection with the points of another ZDAG, D'. This D' is a Heyting Algebra, and our way of interpreting Intuitonistic Predicate Logic on open sets of D translates into a way of interpreting IPL on the points of D'. The operation D ↦ D' gives us lots of examples of planar Heyting Algebras – but not all.

Take any ZDAG D whose points all have the same parity. There is a simple, visual criterion that can tell us very quickly whether D is a HA or not. The ZHAs are the Ds that obey this criterion and the parity condition; an arbitrary ZDAG D is a HA iff it is isomorphic to a ZHA, and this is also easy to check. This gives us all planar Heyting Algebras.

There is a system of coordinates that we can put on a ZHA – the (l,r) coordinates – that make ⊤, ⊥, ∧, ∨, → trivial to calculate. We will present a computer library that does all these calculations, and that can produce ascii and LaTeX diagrams for both ZDAGs and functions on them.

Heyting algebra modalities for children. A modality is an operation ^* on the points of a HA obeying P ≤ P^* = P^** and (P∧Q)^* = P^*∧Q^*. The operations B_⊥(P) = ¬¬P, B_Q(P) ↦ ((P→Q)→Q), J_Q(P) = Q∨P, J^Q(P) = Q→P, are modalities, and our computer library can show visually how they behave on the points of a ZHA and how they can be composed in several ways (as in [FourmanScott79], p.331) to obtain new modalities.

The usual way of presenting HA modalities in the literature is by showing first some basic consequences of the axioms, then how modalities interact with ∧, ∨, →, then theorems about how the algebra of modalities behave; I have always found this approach quite opaque. By using ZHAs we can explain these theorems and exhibit conter-models for all non-theorems visually – and it turns out that modalities on a ZHA D correspond to ways of cutting D into equivalence classes using diagonal lines. This visual way of thinking complements the usual formal way... but how, exactly? Can we make that precise?

Categories for children. For our purposes, the archetypal category is Set, and in most examples we can use only finite subsets of ℕ as its objects in diagrams. This lets us introduce quickly two flavors of typed λ-calculus, the distinction between structure and properties, a trick to focus only on structure and leave the “properties” part for a second moment, and a way to regard having a terminal, binary products, and exponentials – the cartesian-closed structure – as extra structure on Set. A CCC is a category with that extra structure, and by regarding Set as the archetypal case we get a way to interpret the simply-typed λ-calculus formally in any CCC.

It turns out that ZDAGs are categories, and ZHAs are CCCs, both archetypal in slightly weaker ways than Set. By interpreting λ-calculus in ZHAs and making a series of changes in the notation we get the categorical interpretation of intutionistic predicate calculus, plus Natural Deduction, and Curry-Howard.

Toposes for children. Let D be a ZDAG; for example, D = _•^•_•. The category of functors Set^D is a topos – a ZTopos, and its objects are _•^•_•-shaped diagrams that are easy to draw explicitly. CCCs are categories with extra structure that lets us interpret simply-typed λ-calculus on them; toposes are CCCs with extra structure, that lets us interpret Intuitionistic Set Theory (IST) on them. By regarding both Set and our ‘Set^D’s as archetypal toposes we can start topos theory from the “internal language”, i.e., from the way of interpreting all operations of IST in terms of basic categorical operations; our approach lets us begin by examples that show how each operation of IST ought to behave, then guessing a formalization, than proving that it works and thus toposes are models for IST, then proving other facts about toposes that are less logical and more algebraic in character.

Sheaves for children. Each modality on a Heyting Algebra D' induces a notion of “sheafness” on a ZTopos, plus a quotient from it into a “smaller” topos, which has an adjoint that is a functor from the “smaller” topos back into the “bigger” one; the “sheaves” are the objects of Set^D' that are in the image of that adjoint functor.

Using ZToposes as our archetypal toposes we can understand how all these entities and definitions behave by generalizing a few examples where the diagrams are not too big. One nice example – of the logical definition of sheaf – shows how the notion of sheafness induced by B_⊥ booleanizes the logic of a topos; another example, motivated by the topological definition of sheaf, shows how sheafification and étalification are adjoint functors, using an order topology.

The possibilities for exposing tecnicalities using archetypal cases are endless, but we will dedicate the best part of our energy in this tutorial not to them, but to something more general and more useful: how to use archetypal cases to make the literature more accesible, and to create bridges between different notations.

[FourmanScott1979]: M.P. Fourman, D.S. Scott: Sheaves and Logic - in Applications of Sheaves (Springer Lecture Notes in Mathematics 753), pp.302-401

[Ochs2013]: E. Ochs: Internal Diagrams and Archetypal Reasoning in Category Theory - in Logica Universalis, vol 7, issue 3, pp.291-321