Discussing "A Framework for Intuitionistic Modal Logics (Extended Abstract)"

(Link)

Authors: Gordon Plotkin and Colin Stirling (Edinburgh University)

Reference: Plotkin, Gordon, and Colin Stirling. "A framework for intuitionistic modal logics (Extended abstract)". Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pp. 399-406. 1986.

Why this paper? Cited by A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals, Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement, and Intuitionistic versions of modal fixed point logics

Eight years before Alex Simpson’s thesis, which I discussed on this blog just four weeks ago, comes this extremely short (8 pages in a fairly large font!) but groundbreaking paper on intuitionistic modal logics. This paper is specifically the first to look at possible world semantics, also called Kripke semantics after its inventor Saul Kripke, for such logics. I will not repeat the things I said about intuitionistic modal logics in my previous post, but rather focus on this topic of possible worlds semantics.

Classically the truth of a proposition can be calculated based on ‘truth tables’, through which logical connectives can be seen as functions from the propositions they apply to. For example, negation is the function mapping True to False and False to True. The modal connectives Box and Diamond, for necessity and possibility respectively, are not truth-functional in this way. Instead we give meaning to our new connectives by relativising truth to a set of possible worlds, in which a certain proposition might be true in some, but false in others. In fact, a mere set of worlds is not enough; in order to talk sensibly about applying modalities on top of each other, we need to know how the worlds are arranged with respect to relative notions of possibility. For example, if the world Earth-One can be imagined as possible from the world Earth-Prime, does it follow that the inhabitants of Earth-One can imagine the world Earth-Prime? If all worlds have this symmetry, this corresponds to the axiom ‘B’, which states that if a proposition holds, then it necessarily possibly holds. Piling up modalities in this style can, frankly, strain our intuitions, but possible worlds semantics makes things transparent by asking to define the relationship between worlds as part of our definition.

One cool thing about possible worlds semantics is that intuitionistic logic, the logic of constructive reasoning, can also be seen through this lens. Worlds are now viewed as ‘states of knowledge’ and moving from one world to another corresponds to gaining knowledge, for example by discovering a proof of a new mathematical theorem. This setup allows us to give sound and complete semantics for intuitionistic logic (and in particular, its implication connective) within normal mathematics.

What if we wanted to combine the two flavours of logic? Plotkin and Sterling quite correctly predicted that this could have computational significance, an ongoing subject of my own (and others’) work to this day. The aim of this paper was to work out some details of how the Kripke semantics should work for this combination, with an emphasis more on working out a technically reasonable suggestion than on making a philosophical argument. Their suggestion is to have one set of worlds with two relations, one for the modal connectives and one for intuitionistic implication. However possible worlds semantics for intuitionistic logic have the crucial property that moving between worlds cannot falsify previously established truths, but only introduce new ones. If the two relations on worlds are unrelated, this property fails, and so work needs to be done to make them harmonise. A minimal logic (Intuitionistic K, where the K stands for Kripke) is established for these semantics, and some axiomatic extensions such as the B axiom are considered.

Discussing "Categories for the Working Mathematician"

(Link)

Author: Saunders Mac Lane (University of Chicago)

Reference: Mac Lane, Saunders. Categories for the working mathematician. Second Edition. Graduate Texts in Mathematics Vol. 5. Springer-Verlag, 1998 (or for the First Edition, 1971).

Why this paper? Cited by Under Lock and Key: A Proof System for a Multimodal Logic, Groupoid-Valued Presheaf Models of Univalent Type Theory, and KZ-monads and Kan Injectivity

When I started my research career with a Master’s degree at Victoria University of Wellington under the supervision of Rob Goldblatt, this book was not quite where I got started with the fascinating world of category theory (that was Rob’s own wonderful, if somewhat idiosyncratic, Topoi), but was the working reference book I quickly moved to. When Rob and I published my first ever paper (a nice, if not exactly earth-shattering, exploration of collections of coalgebras) we cited this book for some standard definitions and results in category theory we were relying on. This was and remains a typical way to use this book – it has such canonical status that if something in one’s paper relies on something in the book, one can always safely leave its definition to a citation to Mac Lane on the understanding that reviewers and readers should have access to it, preferably in a prominent place on their bookshelf. While I have bought and acquired various reference books over the years, it remains the only one I have ever requested to receive as a Christmas present (thank you to my sister-in-law!). Its iconic status can also be seen from the fact that it is the only abstract mathematics book that I am aware of to have launched a meme, via the quote “All told, a monad in X is just a monoid in the category of endofunctors of X”:
 

Sources: 1 2 3. The word ‘just’ does a lot of work in making this quote funny. Indeed the full exposition about monoids in a category doesn’t come until the chapter after the infamous quote, so the reader could be forgiven for being a little perplexed, let alone the poor functional programmer who just wants to deal with side effects.

Mac Lane was one of the inventors (or discoverers, depending on how one feels about the ontological status of mathematics) of category theory, along with Samuel Eilenberg in 1942. There is no particular rule that the inventor of a discipline will be its best communicator, but surely it doesn’t hurt that Mac Lane maintained an overview of the field from its infancy. The original work was motivated by an attempt to better understand the notion of ‘limit’ in algebraic topology. This led them to formalise the previously informal notion of natural transformation; to get to this, one must first define functor, and to get to that, one must define category. Even though category theory can enter deep and difficult waters, and has a reputation for being hard, the definition of category is startlingly simple and general – a collection of objects, and a collection of arrows between them, obeying identity and associativity rules.

Category theory was “initially… used chiefly as a language” in Mac Lane’s telling, that is a formal language of objects and arrows, from which one can translate back and forth to the sets and elements of ‘normal’ mathematics. It still has that feeling to some extent, as learning category theory after being taught mathematics via sets can indeed feel like learning a second language as an adult. It is often claimed, correctly I think, that a second language can enrich your thinking beyond one’s ability to communicate with a different group of people, because it helps you to organise your thoughts in different ways and hence see the world in different ways. So it certainly is with category theory; armed with the basic definitions, and the knowledge that much of mathematics can be naturally viewed via objects and arrows (typically, some notion of homomorphism or structure-preserving function) one can develop category theory as a topic in its own right, bringing forward new fundamental concepts such as adjunction that do not obviously arise as fundamental when one is thinking in a different mathematical language, but once discovered can be widely and fruitfully applied. The analogy with human languages should not be overdone, of course, because for the most part human languages must be compatible with a variety of viewpoints and personalities, whereas a mathematical language can more strongly bias one to emphasise certain ways of looking at the world. With category theory, one is invited to view the mathematical world in terms of arrows (indeed, Mac Lane shows that one can formulate it without reference to objects at all), so transformations, rather than static elements, become the basis of thought and practice.

This might not be the best book to learn category theory from scratch (I haven’t done a survey of all options, but many speak highly of Awodey’s Category Theory), but once one has the basics down, it gives a clear and readable exposition of many important concepts. It is not impressive in its size and weight in the same manner as Johnstone’s Elephant, but the judicious selection of material for a relatively slim volume is impressive in its own way. It certainly still lives up to its billing as a valuable tool for the working mathematician (or, indeed, theoretical computer scientist) to consult when authors deal with some fundamental piece of category theory by citation.

Discussing "Sketches of an Elephant: A Topos Theory Compendium"

Links: Volume 1 and Volume 2

Author: Peter T. Johnstone (University of Cambridge)

Reference: Johnstone, Peter T., Sketches of an Elephant: A Topos Theory Compendium: Volume 1 and 2. Oxford University Press, 2002

Why this book? Cited by Groupoid-Valued Presheaf Models of Univalent Type Theory, KZ-monads and Kan Injectivity, and Classifying Topoi in Synthetic Guarded Domain Theory

The algorithm I follow to choose topics for this blog, where I take the most highly cited paper from my recent Google Scholar recommendations, can send me off to anything from a short conference paper to a full book. I like the variety, but of course a short blog post can only say so much about a book based on a week of reading pushed in around my other commitments; this was never more true than this week, given the monumental scale and density of these two volumes. The introduction even warns one off reading the book from start to finish; it is intended to be a tome one can dip into to find all manner of important facts in topos theory, including full proof details.

The title of the book refers to the ancient parable of the blind men and the elephant, where men touching different parts of the elephant come to different conclusions about its nature. The book is structured around sections describing the category theoretical notion of topos in different ways - as a category, as a 2-category, as a space, and as a logical theory (the latter being my main focus). The contents for a third volume are also included, covering homotopy / cohomology and mathematical universes, but more than twenty years later this is perhaps as likely to appear as the final Game of Thrones novels – but who knows?

The central definition of a topos in category theory is quite simple for something that can inspire so many pages of work, but this is in keeping with the usual nature of category theory – simple abstract definitions with many examples, which help to organise the structure of mathematical thought and provide connections between apparently unconnected areas. The distinctive concept here is that of subobject classifier, which can be seen as an object of ‘truth values’.  Classically, one can use the two element set of the Booleans True and False, but, to take a contrasting example, in the topos of trees the subobject classifier provides for an infinite-valued logic, as I discussed a few weeks ago. In any topos, the logic provided for by the subobject classifier is at least intuitionistic, but need not be classical (admitting the law of excluded middle, double negation elimination, and so on).

What do I mean by the ‘logic provided for’? To skip ahead to the logic section in the second half of the second book, a lot can be achieved without going all the way to toposes. For example, (sorted) first-order logic of the kind one might be taught in an introductory logic course can be interpreted in any Heyting category, which is a weaker definition than topos. The full power of toposes are not needed to interpret logical theories until one reaches for higher-order logic; in particular the ability to have variables ranging over subsets of a sort (more generally, type), and to sensibly use the set membership symbol ∈, requires the subobject classifier. Having said that, toposes do have their uses as an analytic tool before we get to such powerful logics, as each theory (collection of axioms) expressed with the weaker logics can be aligned to a ‘classifying topos’ which contains a universal model of the theory – a model that satisfies all and only the theorems entailed by the theory.

I should finish by mentioning one of the most stunning achievements of topos theory (to my mind; given the nature of the elephant a topologist would probably come up with something else), which is the connection of the notion of classical logic (certain toposes are Boolean, which means that their underlying logic will be classical) to the axiom of choice much discussed in mathematics. The results, rewarding one for getting 991 pages into the book (or skipping forward to them, as is more to be advised) give a description of Booleans toposes exactly in terms of the choice functions of certain of their objects, and, following Zermelo’s theorem, show that in any topos (including non-Boolean) the objects with choice functions are exactly those that are well-orderable. These results, and others around them, bring a remarkable new clarity to the connections between two of the most discussed concepts in the foundations of mathematics, classicality and choice.

Discussing "Some Properties of Fib as a Fibred 2-category"

(Link)

Author: Claudio Hermida (McGill University)

Reference: Claudio Hermida, Some properties of Fib as a fibred 2-category, Journal of Pure and Applied Algebra, Volume 134, Issue 1, 1999, Pages 83-109

Why this paper? Cited by Semantics for two-dimensional type theory and Linear Dependent Type Theory for Quantum Programming Languages

I generally try to keep the technical content of this blog relatively low; this is a bit of a challenge for a paper like this which focuses on technical development, with most applications and examples left as pointers to the literature. I will at minimum have to assume some familiarity with the mathematical field of category theory to get anywhere with this post.

This paper combines two ideas in category theory, namely fibrations and 2-categories. To get to fibrations, one can (following Chapter 1 of this PhD thesis) start with the notion of an indexed set, which can be defined as a function from a set of elements to an index set. The ‘fibres’ of a certain index are then all the elements that are mapped to that index. A fibration is the categorification of this concept – categorification is not a precise term, but is broadly the process of replacing sets with categories in one’s definitions, usually motivated by a desire for more general results. One here replaces the function between sets with a functor between categories. This move turns out to be fruitful for type theory and (typed first- and higher- order) logic because we can take our index category to be contexts and category ‘above’ to be, for example, where propositions live; the ‘fibres’ then pick out those propositions which make sense in a certain context.

What of 2-categories? One slightly amusing motivation is that sets can be considered 0-categories, ordinary categories as 1-categories, and so 2-categories are merely the categorification of the notion of a category! This makes some sense if one has spent time with categories, as one often talks not just of the categories themselves, and functors between them, but of morphisms between functors, which are called natural transformations (in fact, the historical motivation for the development of category theory was exactly to formalise the notion of natural transformation; some of the other useful terminology was invented as a by-product). The concept of 2-category then gives the general definition for a mathematical structure with that sort of three-level structure of objects, maps between objects, and maps between maps (or if not ‘the’ definition, at least a framework for such definitions, because one in fact gets a few different definitions based on how ‘lax’ or ‘strict’ one wants to be about certain equalities).

This paper’s contribution is to introduce a 2-categorical counterpart of fibrations. The paradigmatic example of such a 2-fibration turns out to be the category Fib of ordinary 1-fibrations, which is fibred over (has an appropriate functor to) the 2-category of categories. At this point one might with some justification feel one’s head start to spin, but Hermida goes on to exploit this viewpoint to prove a variety of theorems about Fib. The value of Fib, to type theory in particular, means that this paper has been steadily cited since its publication, with a modest recent uptick thanks to type theoretic interest in higher categories being driven by research in homotopy type theory.

Discussing "The Proof Theory and Semantics of Intuitionistic Modal Logic"

(Link)

Author: Alex K. Simpson (University of Edinburgh)

Reference: Simpson, Alex K. "The proof theory and semantics of intuitionistic modal logic.", PhD dissertation, University of Edinburgh (1994).

Why this paper? Cited by When programs have to watch paint dry, Wijesekera-style constructive modal logics, and Nested Sequents for First-Order Modal Logics via Reachability Rules

Computer science PhD dissertations, despite being an important part of academic life, are seldom widely read – the work is usually split into more digestible publications in journals and conference proceedings. There are exceptions, however, where the dissertation transcends merely being a stapled-together collection of papers to instead provide a comprehensive overview of a subject at a point of time. This dissertation, with its 557 citations as measured by (the sometimes slightly inaccurate) Google Scholar, is certainly an example of such.

The topic of the dissertation is the merge of intuitionistic logic and modal logic. Intuitionistic logic arose from the constructive mathematics of Brouwer, in which the notion of proof is elevated above the more mysterious notion of mathematical truth. Taking this as our basic logic requires a more restricted logic than is usually accepted, as we reject e.g. double negation elimination, as demonstrating the absence of a disproof does not entail the existence of a proof. Constructivism has become an important topic in computer science because the central concern of our discipline is that which can be constructed (via algorithm). Modal logic is the logic of possibility, necessity, and similar logical connectives. After Kripke (who recently passed away) we think of them as connectives which allow us to discuss `possible worlds’ – a certain thing may be true, but it is only necessarily true if it holds at all possible worlds.

Combining these two logics is a natural thing to do to allow modal connectives to be used in an intuitionistic setting, and has a number of computer science applications, including some that I have published on. The sticking point turns out not to be the ‘box’ operator for necessity (regarding all possible worlds), which has been translated to the intuitionistic setting without controversy many times, but rather the ‘diamond’ operator of possibility (regarding the existence of at least one possible world). Simpson’s first order of business is to survey the literature and make an argument for a particular approach to diamond, which has a range of desirable properties such as distribution over disjunction (if it is possible that A or B holds, then either it is possible that A holds, or possible that B holds).

The bulk of the dissertation revolves around structural proof theory, with natural deduction emphasised. Simpson builds the notion of possible worlds into his proof theory, with explicit requirements to show that certain worlds are possible (more technically, that one world is ‘reachable’ from another). The proof theory is shown to have good properties such as (various notions of) soundness and completeness, and strong normalisation (one can define a proof simplification procedure that is guaranteed to terminate). Most interestingly the proof theory is highly flexible, as a variety of modal logics, differentiated by different notions of the structure of possible worlds, can fit into Simpson’s framework via certain rules that reflect the semantic structure into the proof theory.