This position statement looks back on two decades of work on shallow embeddings of non-classical logics in classical higher-order logic (HOL), a line of research that expanded into a range of logic embeddings in HOL and inspired the LogiKEy logic-pluralistic knowledge representation and reasoning methodology. This paper advances the case for logical pluralism at object-logic level within a unifying meta-logical framework such as LogiKEy, grounding the argument in computational metaphysics. More broadly, it advocates principled support for logical pluralism in modern proof assistants, and cautions against logical imperialism -- the rigid adoption of a single foundational logic for large-scale theory developments -- which impedes the interdisciplinary reuse that LogiKEy is designed to enable.

翻译：这篇立场声明回顾了二十年来在经典高阶逻辑（HOL）中对非经典逻辑进行浅层嵌入的研究工作，该研究方向已扩展至HOL中的一系列逻辑嵌入，并启发了LogiKEy逻辑多元知识表示与推理方法论。本文在LogiKEy这样的统一元逻辑框架内，以计算形而上学为基础，论证了在对象逻辑层面实施逻辑多元主义的合理性。更广泛地说，本文倡导在现代证明助手中对逻辑多元主义提供原则性支持，并警示逻辑帝国主义——即在大规模理论发展中僵化采用单一基础逻辑——这一做法阻碍了LogiKEy旨在实现的跨学科复用。