New Approaches to Modality

I periodically peek at the groundbreaking work on formal systems that is going on in homotopy type theory (HoTT), and in doing so just stumbled on an intriguing treatment of modal HoTT that seems much more philosophically promising to me than standard 20th century modal logic.

Types can be taken as formalizing major aspects of the Aristotelian notions of substance and form. Type theory — developed by Swedish philosopher Per Martin-Löf from early 20th century work by the British philosopher Bertrand Russell and the American mathematician Alonzo Church — is the most important thing in the theory of programming languages these days. It is both a higher-order constructive logic and an abstract functional programming language, and was originally developed as a foundation for constructive mathematics. Several variants of type theory have also been used in linguistics to analyze meaning in natural language.

Homotopy type theory combines this with category theory and the categorical logic pioneered by American mathematician William Lawvere, who was also first suggested a category-theory interpretation of Hegelian logic. HoTT interprets types as paths between topological spaces, higher-order paths between paths, and so on, in a hierarchy of levels that also subsumes classical logic and set theory. It is a leading alternative “foundation” or framework for mathematics, in the less epistemologically “foundationalist” spirit of previous proposals for categorical foundations. It is also a useful tool for higher mathematics and physics that includes an ultra-expressive logic, and has a fully computational interpretation.

There is a pretty readable new book on modal HoTT by British philosopher David Corfield, which also gives a nice introductory prose account of HoTT in general and type theory in general. (I confess I prefer pages of mostly prose — of which Corfield has a lot — to forests of symbolic notation.) Corfield offers modal HoTT as a better logic for philosophy and natural language analysis than standard 20th century first-order classical logic, because its greater expressiveness allows for much richer distinctions. He mentions Brandom several times, and says he thinks type theory can formally capture many of Brandom’s concerns, as I previously suggested. Based on admittedly elementary acquaintance with standard modal logic, I’ve had a degree of worry about Brandom’s use of modal constructs, and this may also help with that.

The worry has to do with a concept of necessity that occasionally sounds overly strong to my ear, and is related to my issues with necessity in Kant. I don’t like any universal quantification on untyped variables, let alone applied to all possible worlds, which is the signature move of standard modal logic. But it seems that adding types into the picture changes everything.

Before Corfield brought it to my attention, I was only dimly aware of the existence of modal type theory (nicely summarized in nLab). This apparently associates modality with the monads (little related to Leibnizian ones) that I use to encapsulate so-called effects in functional programming for my day job. Apparently William Lawvere already wrote about geometric modalities, in which the modal operator means something like “it is locally the case that”. This turns modality into a way of formalizing talk about context, which seems far more interesting than super-strong generalization. (See also Modality and Variation; Deontic Modality; Redding on Morals and Modality).

It also turns out Corfield is a principal contributor to the nLab page I previously reported finding, on Hegel’s logic as a modal type theory.

Independent of his discussion of modality, Corfield nicely builds on American programming language theorist Robert Harper’s notion of “computational trinitarianism”, which stresses a three-way isomorphism between constructive logic, programming languages, and mathematical category theory. The thesis is that any sound statement in any one of these fields should have a reasonable interpretation in both of the other two.

In working life, my own practical approach to software engineering puts a high value on a kind of reasoning inspired by a view of fancy type theory and category theory as extensions or enrichments of simple Aristotelian logic, which on its formal side was grounded in the composition of pairs of informally generated judgments of material consequence or material incompatibility. I find the history of these matters fascinating, and view category theory and type theory as a kind of vindication of Aristotle’s emphasis on composition (or what could be viewed as chained function application, or transitivity of implicit implication, since canonical Aristotelian propositions actually codify material inferences) as the single most important kind of formal operation in reasoning.

Aristotelian Propositions

Every canonical Aristotelian proposition can be interpreted as expressing a judgment of material consequence or material incompatibility. This may seem surprising. First, a bit of background…

At the beginning of On Interpretation, Aristotle says that “falsity and truth have to do with combination and separation” (Ch. 1). On its face, the combination or separation at issue has to do not with propositions but with terms. But it is not quite so simple. The terms in question are canonically “universals” or types or higher-order terms, each of which is therefore convertible with a mentioned proposition that the higher-order term is or is not instantiated or does or does not apply. (We can read, e.g., “human” as the mentioned proposition “x human”.) Thus a canonical Aristotelian proposition is formed by “combining” or “separating” a pair of things that are each interpretable as an implicit proposition in the modern sense.

Propositions in the modern sense are treated as atomic. They are often associated with merely stipulated truth values, and in any case it makes no sense to ask for internal criteria that would help validate or invalidate a modern proposition. But we can always ask whether the combination or separation in a canonical Aristotelian proposition is reasonable for the arguments to which it is applied. Therefore, unlike a proposition in the modern sense, an Aristotelian proposition always implicitly carries with it a suggestion of criteria for its validation.

The only available criteria for critically assessing correctness of such elementary proposition-forming combination or separation are material in the sense that Sellars and Brandom have discussed. A judgment of “combination” in effect just is a judgment of material consequence; a judgment of “separation” in effect just is a judgment of material incompatibility. (This also helps clarify why it is essential to mention both combination and separation affirmatively, since, e.g., “human combines with mortal” canonically means not just that human and mortal are not incompatible, but that if one is said to be human, one is thereby also said to be mortal.)

This means that Aristotle’s concept of the elementary truth and falsity of propositions can be understood as grounded in criteria for goodness of material inference, not some kind of correspondence with naively conceived facts. It also means that every Aristotelian proposition can be understood as expressing a judgment of material consequence or incompatibility, and that truth for Aristotle can therefore be understood as primarily said of good judgments of material consequence or incompatibility. Aristotle thus would seem to anticipate Brandom on truth.

This is the deeper meaning of Aristotle’s statement that a proposition in his sense does not just “say something” but “says something about something”. Such aboutness is not just grammatical, but material-inferential. This is in accordance with Aristotle’s logical uses of “said of”, which would be well explained by giving that a material-inferential interpretation as well.

The principle behind Aristotelian syllogism is a form of composition, formally interpretable as an instance of the composition of mathematical functions, where composition operates on the combination or separation of pairs of terms in each proposition. Aristotelian logic thus combines a kind of material inference in proposition formation and its validation with a kind of formal inference by composition. This is what Kant and Hegel meant by “logic”, apart from their own innovations.