Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913164360155136 |
|---|---|
| author | Benzmüller, Christoph Kirchner, Daniel Pasetto, Luca |
| author_facet | Benzmüller, Christoph Kirchner, Daniel Pasetto, Luca |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_27246 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint) Benzmüller, Christoph Kirchner, Daniel Pasetto, Luca Logic in Computer Science Artificial Intelligence Logic 03Axx, 03Bxx, 03B15, 68T15 F.4; I.2.3; I.2.4 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. |
| title | Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint) |
| topic | Logic in Computer Science Artificial Intelligence Logic 03Axx, 03Bxx, 03B15, 68T15 F.4; I.2.3; I.2.4 |
| url | https://arxiv.org/abs/2605.27246 |