This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic multiplicative linear logic. Next to these meta-logical-investigations, we contribute to building an Isabelle category theory library, with a focus on ease of use in the formalization beyond category theory itself. This work paves the way for future formalizations based on category theory and demonstrates the power of automated reasoning in investigating meta-logical questions.

翻译：本文基于范畴论，利用证明助手Isabelle/HOL开展元逻辑研究。通过形式化基本拓扑（elementary topos）的概念，我们展示了基于自由逻辑的浅层语义嵌入范畴论的潜力。此外，我们形式化了对称幺半封闭范畴（symmetrical monoidal closed categories），表达了直觉主义乘法线性逻辑的指称语义模型。除这些元逻辑研究外，我们还为构建Isabelle范畴论理论库做出贡献，重点在于使其在超越范畴论本身的形式化应用中易于使用。这项工作为未来基于范畴论的形式化研究铺平了道路，并展示了自动推理在探究元逻辑问题中的强大能力。