Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)
For researchers in formal methods and knowledge representation, this paper provides a conceptual argument for logical pluralism, though it is a position statement rather than a novel technical contribution.
This position paper advocates for logical pluralism in formalised reasoning, arguing against the rigid adoption of a single foundational logic. It reviews two decades of work on shallow embeddings of non-classical logics in classical higher-order logic, culminating in the LogiKEy methodology, and calls for principled support of multiple logics in proof assistants.
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.