On 18 Nov 2022, at 11:16, Michael Shulman wrote:
On Fri, Nov 18, 2022 at 2:59 AM Jon Sterling <jon@jonmsterling.com> wrote:Hi Mike, thanks for your comments — regarding modal type theory, please note that there are state of the art general modal type theories that do not employ admissible substitution! MTT is one of them.Split-context modal type theories can also be presented without admissible substitutions. Making substitutions explicit is easy; it's making them admissible that's hard. And as far as I understand it, MTT does satisfy the primary desideratum when making substitutions admissible, namely that all rules have a fully general context in their conclusion.MTT is also not equivalent to split-context theories, and IMHO is less pleasant to work with in practice. I believe there should be some way to combine the ideas of the two theories.By the way, in the followup paper "Modalities and parametric adjoints" by Gratzer, Cavallo, Kavvos, Guatto, and Birkedal (three of whom are also authors of the MTT paper) we read "The admissibility of substitution is a central property of type theory, and indeed of all logic" (section IB).
The real reason it is central is that making substitution admissible forces you to figure out the equational theory of substitutions (as I said), not the other way around. You are free to consult the other authors of that paper, and I guarantee to you that they will confirm my analysis. Admissibility seems to have been cargo-culted, as people forgot the reason why it was important in the first place.
It is important to recall that the first admissible rule was *cut* in Gentzen's analysis of sequent calculus, but Gentzen's cut-free sequent calculus is eliminating not only substitution but also all computational redexes simultaneously (this is due to the way that sequent calculus is arranged). This kind of admissibility is much more useful than mere admissibility of substitution, because it gives a normal-forms presentation, which (unlike mere admissible substitution) actually has a ton of practical applications (not just deciding equivalence, but also proof search, etc.). So I would characterize my viewpoint as an essentially orthodox one, though the language we use to say these things in 2022 is very different from what was available in the 1930s.