对于类型论的元理论，内部 sconing 已足够
计算机科学中的逻辑
2023-05-10 v2 范畴论
摘要
关于类型论的元定理通常通过将其语法解释到使用范畴粘合构造的模型中来证明。我们提议仅使用 sconing（沿全局截面函子的粘合）而非一般的粘合。该 sconing 在预层范畴内部执行，并通过外部化恢复原始的粘合模型。我们的方法依赖于涉及两类模型概念的构造：一阶模型（含显式上下文）与高阶模型（无显式上下文）。Sconing 将一个显示的高阶模型转化为显示的一阶模型。利用这些，我们推导出类型论语法的专门归纳原理。此类归纳原理的输入是其动机与方法的无样板描述，不提及上下文；输出是一个具有以同一内部语言指定的计算规则的截面。我们通过类型论的正则性、规范化与语法参数性的证明来说明我们的框架。
引用
@article{arxiv.2302.05190,
title = {For the Metatheory of Type Theory, Internal Sconing Is Enough},
author = {Rafaël Bocquet and Ambrus Kaposi and Christian Sattler},
journal= {arXiv preprint arXiv:2302.05190},
year = {2023}
}