### 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…)

## Comments

## Post a Comment