Mark Jago on Type Theory in Computer Science, Logic and Linguistics

February 19, 2026

First an introduction:

This is great! For a long time I have been thinking that someone (I guess it's me!) should produce a system that allows people who are studying these different logical formalisms to fairly easily write formal descriptions of translations from one to the other and also to formally prove things about the translations and maybe about these translation processes themselves (You would want a very expressive system like HoTT with Univalence to do this though. See Voevodsky's comment at 2016 Heidelberg Laureate Forum "... it came out, as a result of practical work on formalization we just discovered that the law of excluded middle and axiom of choice can be avoided in the univalent foundations much more successfully than they can be avoided in set theory, so things which can not be done without them in set theory can be done without them in the univalent foundations, so then there was this understanding that the classical mathematics appears as a subset of this new constructive mathematics. That is actually kind of an easy easy thing to see, but it's important to emphasize that one obtains the view of mathematics as constructive and then the classical mathematics as a subset of this constructive mathematics, a very important subset, and it's kind of a retract: it's not only a subset but it's it's a retract, but it's still a subset" And he goes on: "The understanding that the MLTT extended with the UA is an imperfect formalization system for this constructive mathematics and that it should be possible to integrate the UA into the MLTT obtaining a new type theory with better computational properties."). Wouldn't it be great to be able to write down a formal specification of the language of Principia Mathematica and Church's Simple Theory of Types and then see what proofs look like in each? You could also start to think about questions like "How do higher equality types in HoTT relate to Ramification in Principia Mathematica?"

See Emily Riehl on Univalent Foundations.

The linguistics stuff is really interesting:

Higher-order Logic and Type Theory: 10:14 "In some ways modern compositional semantics is just applying type theory and possible-world semantics to natural language, ..." so systems like the one I described above would be useful in science too: Maria Violaris Interview With Tony Short on Probability in the Many Worlds nterpretation of Quantum Mechanics also Christine Aidala and Gabriele Carcassi on Foundations of Physics and Assumptions of Physics - Reading the Book.

Then his video on Meaning in Logic:

18:09 On proof-theoretic interpretations of logic and "the know-ability problem", see the commentary on Quine's Confirmation Holism. If you take Quine seriously, then underdetermination of our belief in whatever knowledge we have obtained from logical inference is dependent on much more than just our position as regards the semantic content of some particular logical formalism.

My comment:

20:00 On what constitutes meaning in Logic. I think it is a lot of things. I think that it depends on what you are doing with the logic. For example, if you want to use logic to reason "metamathematically" about what is and is not within the power of reason to determine, then you need to have some sort of descriptive content in your semantics. You want at least to be able to restrict your statements to meaningful formulae, ... I am thinking of some well-known constructions of sentences in Arithmetic, for example, that have distinct but contradictory meanings, and have been deliberately constructed in that way to "prove" something about what is and is not provable in some formal system! But if you are looking for a way to formalise statements in first order Arithmetic then the standard Tarskian definition of truth for first order languages will do as a way to describe the meaning of arithmetic formulae in set theory or whatever is your metalanguage, and then the meaning of your formulae can in some sense be said to 'reduce' to just the truth or falsity of the statements. This doesn't work for metamathematics though and it seems so obvious to me that I think it must be some kind of sick joke that got completely out of hand and now nobody can bring themselves to call it out for what it is.

See https://www.markjago.net/.

Subscribe to Attic Philosophy.

Here's a nice example of how much insight you can get by reinterpreting one language in another: see also Zainab Ali - Recursion Schemes from First Principles.

This was from a 2017 series of lectures Vladimir Voevodsky Memorial Conference.

Subscribe to Institute for Advanced Study.

And I discovered another nice example in something called "The Calculus of Dependent Lambda Eliminations" which is implemented by a program called Cedille: https://cedille.github.io/