以 Isabelle/HOL 中的范畴论作为元逻辑研究的基础
计算机科学中的逻辑
2023-10-20 v2 范畴论
逻辑
摘要
本文提出基于范畴论并使用证明辅助工具 Isabelle/HOL 的元逻辑研究。我们通过给出初等拓扑斯（elementary topoi）概念的形式化，展示了基于自由逻辑的浅语义嵌入范畴论的潜力。此外，我们形式化了对称幺半闭范畴，其表达了直觉主义乘法线性逻辑的指称语义模型。除这些元逻辑研究外，我们致力于构建 Isabelle 范畴论库，重点关注在范畴论本身之外形式化中的易用性。本工作为未来基于范畴论的形式化铺平了道路，并展示了自动化推理在研究元逻辑问题中的能力。
引用
@article{arxiv.2306.09074,
title = {Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation},
author = {Jonas Bayer and Aleksey Gonus and Christoph Benzmüller and Dana S. Scott},
journal= {arXiv preprint arXiv:2306.09074},
year = {2023}
}
备注
15 pages. Preprint of paper accepted for CICM 2023 conference