数学证明助手在逻辑教学中的应用：LogiKEy方法论
Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology
- Otto-Friedrich-Universität Bamberg（奥托-弗里德里希-班贝格大学）
- Freie Universität Berlin（柏林自由大学）
- University of Luxembourg（卢森堡大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文介绍基于LogiKEy方法，利用经典高阶逻辑和证明助手Isabelle/HOL教授多元逻辑，通过系列谜题展示从命题到道义逻辑的教学路径，并反驳单一主义质疑，强调其可移植性。
AI中文摘要：
我们报告了一种向计算机科学、数学和哲学混合学生群体教授逻辑的方法，该方法基于逻辑多元主义的LogiKEy方法论，已在课程、暑期学校和教程中使用了十多年。LogiKEy使用经典高阶逻辑（HOL）作为通用元逻辑，在其中通过定义语义来编码对象逻辑（包括经典和非经典逻辑）；通过这些语义嵌入，单个证明助手（例如Isabelle/HOL）及其自动化定理证明器和（反）模型查找器，成为学生在一个环境中学习、实验和比较逻辑的平台。在论证了证明助手在逻辑课堂中的教学价值之后，我们呈现了一系列分级课堂示例，每个过渡都由先前表示的局限性、对更明确建模资源的需求或新应用所驱动。一个说谎者与说真话者谜题从命题逻辑引导到模态逻辑；智者谜题引导到动态认知逻辑；Boolos的好奇推理说明了高阶元逻辑在自动化证明搜索中的价值；Chisholm悖论将序列引入道义逻辑，并从标准道义逻辑扩展到二元道义逻辑；而Gödel的本体论论证将其带到研究级别的形而上学论证。然后，我们反驳了将所有内容嵌入经典HOL是单一主义而非多元主义的反对意见，反思了三年教授此类课程的经验，并概述了该方法在Isabelle之外的便携性。
英文摘要：
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.
