Logic teaching method unifies multiple logics in one tool
Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology
Artificial IntelligenceLogic in Computer Science
Summary
Teaching logic can be complicated because there are many different types of logic, like classical, modal, and deontic. The authors present a way to teach these diverse logics using one proof assistant tool by encoding them all in a universal logical framework called higher-order logic. This lets students explore and compare different logics interactively, using puzzles and examples that increase in complexity. Their decade-long experience shows this method supports learning a wide range of logical reasoning styles in one environment.
What this means in practice
- •For logic course instructors: Use a single proof assistant environment to effectively teach multiple types of logic to diverse student groups in a unified way.
- •For formal methods engineers: Experiment with different logical frameworks within one tool to model and verify system properties that require classical and non-classical reasoning.
Authors
Christoph Benzmüller, David Fuenmayor, Luca Pasetto
Abstract
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ödel'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.