# Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 72 references that are in the map.
- First posted on arXiv 6 Oct 2026.

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

- [Faithful Logic Embeddings in HOL -- Deep and Shallow](https://mlsanity.com/paper/2502.19311/) (2025)
- [The TPTP Format for Interpretations](https://mlsanity.com/paper/2406.06108/) (2024)
- [Logical Modalities within the European AI Act: An Analysis](https://mlsanity.com/paper/2501.19112/) (2025)
- [Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)](https://mlsanity.com/paper/2605.27246/) (2026)
- [Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers](https://mlsanity.com/paper/2208.06879/) (2022)
- [Proof Assistants for Teaching: a Survey](https://mlsanity.com/paper/2505.13472/) (2025)
- [Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)](https://mlsanity.com/paper/2609.07345/) (2026)
- [G"odel's and Scott's Variants of the Ontological Argument in Lean 4 and TPTP THF](https://mlsanity.com/paper/2609.26806/) (2026)

## Abstract (arXiv)

We report on an approach to teaching logic to mixed groups of computer science, mathematics, and philosophy students, based on the logico-pluralistic LogiKEy methodology, used for more than a decade in courses, summer schools, and tutorials. LogiKEy uses classical higher-order logic (HOL) as a universal metalogic in which object logics, classical and non-classical alike, are encoded by defining their semantics; through these semantical embeddings a single proof assistant (e.g. Isabelle/HOL), with its automated theorem provers and (counter-)model finders, becomes one environment in which students learn, experiment with, and compare logics. After making the pedagogical case for proof assistants in the logic classroom, we present a graded sequence of classroom examples, each transition motivated by a limitation of the preceding representation, by a need for more explicit modelling resources, or by a new application. A liars-and-truth-tellers puzzle leads from propositional to modal logic; the Wise Men puzzle leads on to dynamic epistemic logic; Boolos's curious inference illustrates what a higher-order meta-logic buys, even for automated proof search; Chisholm's paradox takes the sequence into deontic logic, and from standard to dyadic deontic logic; and G"odel's ontological argument brings it to a research-level metaphysical argument. We then rebut the objection that embedding everything in classical HOL is monism rather than pluralism, reflect on three years of teaching such a course, and sketch the portability of the approach beyond Isabelle.