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开展元逻辑研究。我们通过形式化基本拓扑斯的概念，展示了基于自由逻辑的范畴论浅层语义嵌入的潜力。此外，我们形式化了表达直觉主义乘法线性逻辑指称语义模型的对称幺半群闭范畴。除这些元逻辑研究外，我们还致力于构建Isabelle范畴论库，重点关注在范畴论本身之外的形式化中易于使用。这项工作为未来基于范畴论的形式化研究铺平了道路，并展示了自动推理在探究元逻辑问题方面的强大能力。