One reason (among many) to like Homotopy Type Theory

(Cross-posted at NewAPPS)

Last week I was in Munich for the excellent ‘Carnap on logic’ conference, which brought together pretty much everyone who’s someone in the world of Carnap scholarship. (And that excludes me -- still don’t know exactly why I was invited in the first place…) My talk was a comparison between Carnap’s notion of explication and my own conception of formalization, as developed in my book Formal Languages in Logic. In particular, I proposed a cognitive, empirically informed account of Carnap’s notion of the fruitfulness of an explication.

Anyway, I learned an awful lot about Carnap, and got to meet some great people I hadn’t yet met. But perhaps the talk I enjoyed most was Steve Awodey’s ‘On the invariance of logical truth’ (for those of you who have seen Steve lecturing before, this will come as no surprise…). The main point of Steve’s talk was to defend the claim that the notion of (logical) invariance that is now more readily associated with Tarski, in particular his lecture ‘What are logical notions?’ (1966, published posthumously in 1986), is already to be found in the work of Carnap of the 1930s. This in itself was already fascinating, but then Steve ended his talk by drawing some connections between the invariance debate in philosophy of logic and his current work on homotopy type theory. Now, some of you will remember that I am truly excited about this new research program, and since I’ve also spent quite some time thinking about invariance criteria for logicality (more on which below), it was a real treat to hear Steve relating the two debates. In particular, he gave me (yet another) reason to be excited about the homotopy type theory program, which is the topic of this blog post.

For those of you not familiar with the debate on invariance criteria for logicality, here’s a short primer. In his 1966 lecture, Tarski proposed permutation invariance as a sound criterion for what should count as a logical notion, under the argument that permutations are the most general transformations, and thus that permutation invariance is an adequate formal explanans for the informal notion of the generality of logic. But as noted by Tarski himself in the lecture, the permutation invariance criterion yields a class of putative ‘logical constants’ that are essentially only sensitive to the number of elements in classes of individuals.

It turns out that our logic is even less than a logic of extension, it is a logic of number, of numerical relations… It turns out that the only properties of classes (of individuals) which are logical are properties concerning the number of elements in these classes. (Tarski 1966/86, 151)

In recent decades, a wealth of papers on the issue of the demarcation of logic and different criteria of invariance has ensued, involving in particular people such as Gila Sher, Sol Feferman, John MacFarlane, Denis Bonnay, among others. Much of this literature is concerned with the fact that the straightforward invariance criterion proposed by Tarski counts too much of mathematics as belonging to the realm of logic, thus overgenerating with respect to the target concept (logicality). This has prompted the formulation of a number of modified invariance criteria. However, hardly anyone seems to have worried about the phenomenon of undergeneration, i.e. the fact that the criterion excludes from the realm of logic theories and notions that we may want to count as logical for independent reasons. This is what motivated me to write my paper ‘The undergeneration of permutationinvariance as a criterion of logicality’ (forthcoming in Erkenntnis), where I take work by MacFarlane, van Benthem and others as my starting point to discuss the case of modal logics which do not pass the invariance test for logicality.

My general point in the paper is that these Tarskian invariance criteria restrict the realm of logic to phenomena that pertain to numbers, quantification, and the cardinality of sets and classes. As such, they fail to capture a lot of what we may want to put under the heading of logic, while counting a lot of mathematics as logic. This is simply because numbers and quantification are arguably not all there is to logic.

Where does homotopy type theory come in? As Steve explained in his talk (and as described in the HoTT book right at the beginning, p. 3), homotopy type theory relies on the notion of its logical constructions as being homotopy-invariant on the spaces of homotopy theory. So logicality is associated with an invariance criterion, namely homotopy-invariance, but this criterion does not require sameness of cardinality/number for the transformations in question. Steve’s example was of the transformation of a sphere into a point, which is homotopy-invariant but does not require preservation of cardinality. (Unfortunately, for now I’m still not entirely clear on what exactly counts as a 'homotopy-invariant construction', so I can’t provide further details at this point. Ask Steve!) Now, for those of us who think that what is wrong with Tarskian invariance criteria is that what they deliver are “logics of number”, this is an excellent reason to like the notion of logicality emerging from homotopy type theory.

The catch is that, given that homotopy type theory is a program in the foundations of mathematics, one of the upshots is that the program is not in the least bit interested in providing a criterion demarcating logic from mathematics. As mentioned above, this is a worry that motivated much of the recent work on invariant criteria, in particular Feferman’s work, where one finds the complaint that Tarskian invariance counts too much of what is properly mathematical as logical. (By contrast, Gila Sher sees this as an advantage of the proposal, in that it yields a picture of logic and mathematics as forming a continuum.) But for those of us who worry more about undergeneration than about overgeneration (and I may well be the sole inhabitant of this peculiar class), the notion of homotopy-invariance looks very promising as a technical means to further investigate the nature of logic as such (given that it is not based on the notion of sameness of cardinality between classes).

(And on this note, let me go read the HoTT book…)