# Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)

arXiv: https://arxiv.org/abs/2605.27246 · HTML: https://mlsanity.com/paper/2605.27246/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 38 references that are in the map.
- First posted on arXiv 26 May 2026.

## Builds on (most cited first, 5 of 5)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Extensional Higher-Order Paramodulation in Leo-III](https://mlsanity.com/paper/1907.11501/) (2019)
- [Faithful Logic Embeddings in HOL -- Deep and Shallow](https://mlsanity.com/paper/2502.19311/) (2025)
- [Solving Quantified Modal Logic Problems by Translation to Classical Logics](https://mlsanity.com/paper/2212.09570/) (2022)
- [Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of G"odel's Ontological Argument](https://mlsanity.com/paper/1910.08955/) (2019)

## Built on by (most cited first, 2 of 2)

- [Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)](https://mlsanity.com/paper/2609.07345/) (2026)
- [Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology](https://mlsanity.com/paper/2610.08214/) (2026)

## Abstract (arXiv)

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.