Discussing "The Simplicial Model of Univalent Foundations (after Voevodsky)"

(Link)

Authors: Krzysztof Kapulkin (University of Pittsburgh) and Peter LeFanu Lumsdaine (Institute for Advanced Study)

Reference: Krzysztof Kapulkin, Peter LeFanu Lumsdaine, The simplicial model of Univalent Foundations (after Voevodsky). J. Eur. Math. Soc. 23 (2021), no. 6, pp. 2071–2126. DOI 10.4171/JEMS/1050

Why this paper? Cited by Normalization and coherence for ∞-type theories, The Formal Theory of Monads, Univalently, and On the ∞-topos semantics of homotopy type theory

This paper has a rather peculiar publication history, as it started as a 2012 preprint written by the two authors along with a third, Fields medal winning mathematician Vladimir Voevodsky, who was in fact the main author. However Voevodsky grew disenchanted with the paper due to some issues with the type theory literature it was relying on, and asked for his name to be removed. Sadly, Voevodsky passed away before rectifying these holes in the literature, and so Kapulkin and Lumsdaine worked the paper into a publication. Lacking permission to re-add Voevodsky’s name to the author list, his contribution is instead recognised in the title.

One benefit of this paper having almost a decade to germinate is that it has a particularly pleasant and well written introduction to its topic, Homotopy Type Theory (HoTT). I looked at the seminal HoTT book on this blog last year; this paper picks up one of the topics that the book does not address, although it is briefly mentioned, namely denotational semantics. To recap, HoTT is an approach to mathematical foundations that aims to be both usable by humans and amenable to computer formalisation. The technical approach is to extend previous approaches to type theory with, in particular, a property called the univalence axiom (the other major innovation, higher inductive types, are not discussed here).  Univalence strengthens the usual notion of equality in type theory to, at the type level, correspond to equivalence; this means that one can move constructions and results between equivalent mathematical settings, a common feature of mathematical argument, ‘for free’. This leads one to think of types as (some sort of topological) space, with equality as paths in a space à la homotopy theory.

This paper makes this connection formal by giving homotopy type theory denotational semantics in the category of simplicial sets. Denotational semantics give a mathematical meaning for the constructions of a type theory, programming language, or logic. So long as the mathematical model chosen is not pathological, this gives us as immediate benefit a proof of consistency (one cannot prove false, or construct an element of a type that should be empty). Just as importantly, this style of semantics assures us that all syntactic constructions are not mere shuffling of symbols, but have real mathematical meaning that can be communicated to someone who is not necessarily interested in the details of the particular type theory. Put another way, the type theory is ‘about something’ other than itself.

Why is the ‘something’ that HoTT is about in this paper – i.e. simplicial sets – actually interesting, beyond mere proof of consistency? This paper does not offer an introduction to this mathematics, but looking at one of the books cited as background (link to pdf) gives some clues: “the category of simplicial sets has a homotopical structure … the resulting homotopy theory is equivalent in a strong sense to the ordinary homotopy theory of topological spaces… Insofar as simplicial sets are algebraically defined, and the corresponding closed model structure is combinatorial in nature, we obtain an algebraic, combinatorial model for standard homotopy theory”. In other words, simplicial sets are not a mere mathematical curiosity than happens to work for this type theory, but rather a strongly motivated approach to the general study of homotopy which, of course, is what motivated homotopy type theory in the first place. It should be noted that simplicial sets are not unique in having this property; there is a somewhat similar structure called cubical sets that appear to be more suited to computational implementation. But that, perhaps, is a story for another day.

Discussing 'Display Logic'

(Link).

Author: Nuel D. Belnap, Jr. (University of Pittsburgh)

Reference: Journal of Philosophical Logic vol. 11(4), pp. 375-417 (1982).

Why this paper? Cited by 7 (of a possible 29) of the papers in my Google Scholar Updates recommendations.

Comments: This week's paper is perhaps best understood as standing at the crossroads of two of the biggest features of modern logic (by which I mean, roughly, logic since Gödel blew everything up).

The first is that modern logicians are interested in structured proofs. Rather than attempting to proceed from axioms to conclusion in an undirected way, it can be useful to lock ourselves in to a system which tightly constrains what steps we may make within our proof, and hence prevents us from getting lost. Such structure can in particular guide automated proof search, i.e. the question of how one writes computer programs to do proofs automatically. This is vital for proving properties of, for example, massive software, where the sheer scale would defeat any human effort even if each individual step is quite simple-minded. The godfather of this field of structural proof theory is Gerhard Gentzen, who in the mid 30s invented not one but two of the most important proof systems we work with to this day: natural deduction, which is supposed to formally capture the way humans reason, and his sequent calculus, which is particularly useful for proving certain properties of logics such as their consistency, and provides the basis for some automated provers.

Gentzen was only interested in two sorts of logic - classical and intuitionistic. Modern logicians do not have it so easy, as the second feature I want to highlight is the dizzying and constantly increasing variety of different logics out there, sporting all sorts of different notions of truth, inference, meaning, and so forth. Many logics are created to meet some specific application; computer science leads the pack here, but philosophers are also prolific inventors of new logics, and other areas like linguistics, mathematics, and physics chip in too. Still other logics are invented for entirely 'pure' reasons, with logicians twiddling with the settings of existing logics to see what pops out (and this style of logic research has seen the invention of logics that later found important concrete applications).

There is a tension between these desires for structure and novelty - the more controlled the proof system, the less likely it is that your wacky new logic can be fitted to it. This has led to a variety of extensions of Gentzen's ideas to make them flexible enough to fit a wider variety of logics, and Belnap's display calculus, introduced in this 1982 paper, is the most flexible I know of. This made it the perfect basis for the paper I wrote last year with some co-authors at Australian National University, where we used display calculus to give a structured proof system for a logic called 'Full Intuitionistic Linear Logic' whose proof theory had previously been a rather awkward business (hence, of course, the occurrences of this citation in my Google Scholar Updates recommendations).

Display calculus is an extension of Gentzen's sequent calculus. A sequent is a set of assumptions and conclusions, possibly with some structure imposed on them such as an ordering. Display calculus uses more richly structured sequents which sport the display property, a technical property which allows any assumption or conclusion you have in your current sequent to be 'displayed' so that it becomes the ongoing focus of your calculations, with all other parts of your sequent set to one side. The cool things about this setup are first, that an enormous variety of logics can be given display calculi (though by no means all; Belnap himself mentions quantum logic as something which he couldn't fit into his structure). Second, any calculus with the display property is guaranteed to have a certain property called cut-elimination which is extremely useful for proving all sorts of things about your logic, but which can often be extremely tricky to prove from scratch. So using display calculus can save a lot of work! Of course, nothing comes for free, and display calculi do have limitations, such as not being much use as a basis for automation. But they are still a useful tool to know about for the logician hoping to tame the jungle of logics that are out there.