Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology

1 The Logic Pluralism Challenge in Logic Education

• Students from computer science, mathematics, linguistics, and philosophy bring different backgrounds, motivations, and tolerances for formalism to a demanding subject.Their experience ranges from programming without proof-writing to philosophical argument without comfort with quantifiers.Source: §1 · p. 2
• Teaching non-classical logics separately can make each one feel like a fresh start and obscure what logics share and how they differ.Applications in AI, natural-language semantics, and law and ethics often require reasoning beyond classical first-order logic.Source: §1 · p. 2
• LogiKEy defines object-logical semantics within classical HOL, letting one proof assistant support learning, experimentation, and comparison across logics.The environment includes automated theorem provers and (counter-)model finders.Source: §1 · p. 2
• The chapter presents a graded path from logic puzzles to research-level ethics and metaphysics, with transitions motivated by limits of prior representations, modelling needs, or new applications.It also describes supporting tools and reflects on three years of teaching the course to a mixed audience.Source: §1 · p. 3
• The chapter’s new contribution is the worked course and rationale, tools for non-specialists, response to the monism objection, and sketch of portability beyond Isabelle.It presents a methodological infrastructure and teaching application, not an empirical study of learning.Source: §1 · p. 3
• Students need no prior Isabelle, type-theory, or programming knowledge, but instructors must invest time in adopting the tools.The machine-checked course sources are openly available.Source: §1 · p. 3

2.1 Higher-order logic as a universal meta-logic

• HOL supports LogiKEy as a universal meta-logic because students can quantify over predicates and functions and use λ-abstraction to define compositional encodings.Students encounter its higher-order features as needed, without prior type-theory knowledge.Source: §2.1 · p. 4

2.2 Semantical embeddings, by example

• Shallow semantical embedding represents modal propositions as world-predicates and necessity as truth at all accessible worlds, allowing HOL provers and model finders to work on modal facts.Changing frame conditions yields different logics; the figure shows reflexivity validating □ϕ →ϕ and its failure producing a countermodel.Source: §2.2 · pp. 4–5, Figure 1 · p. 5

2.3 A layered architecture—and why it helps

• The four-layer architecture runs from HOL through object logics and domain theories to concrete scenarios, allowing students from different disciplines to enter at a fitting layer.The layers provide a shared platform and underlying language despite different points of entry.Source: §2.3 · p. 5, Figure 2 · p. 6

2.4 Semantical embeddings and logical pluralism

• Shallow embeddings let provers work directly on object formulas, while deep embeddings treat syntax as data; for simple logics, the two styles are faithful and validate the same formulas [7].Embedding also supports reasoning about the logic itself, including frame correspondences and countermodels when they fail.Source: §2.4 · p. 6, Figure 3 · p. 7
• LogiKEy treats logics as definitional variants that can be compared, combined, and revised within one framework, rather than crowning HOL as the one true logic.The object logic, and to some extent the meta-logic, remain negotiable and open to study.Source: §2.4 · pp. 6–7

Status of the claims

• The research-oriented teaching rationale builds on prior theorem-prover teaching work, but the pedagogical claims rest on small, self-selected cohorts and are offered as hypotheses, not controlled-study findings.The authors describe three runs of one course, alongside earlier courses in the same line.Source: §3 · p. 8

Immediate, machine-checked feedback

• Immediate checking exposes errors in apparently obvious reasoning and clarifies where an inference's real content lies.Every step is checked as it is made, rather than receiving feedback days later, if at all.Source: §3 · p. 8

Logic as an experimental subject

• Proof search and model finding let students experiment with formulae, frame conditions, and axioms, supporting conjecture-and-test practice.The section gives questions about frame classes, seriality, and distinguishing modal logics S4 and S5 as examples.Source: §3 · p. 8

What students actually do

• Students formalise informal puzzles, principles, or rules, then test and revise them with machine feedback, practising movement between natural language and formal notation.The authors describe this iterative process as computational hermeneutics: successive accepted and rejected formalisations make an informal concept explicit.Source: §3 · pp. 8–9

A dialogical style of learning

• A proof assistant can serve as the machine partner in a learner dialogue, while interpreting feedback and connecting it to the underlying question remains the student's work.An Isabelle theory can preserve accepted steps and unsuccessful attempts as a formally verified learning journal.Source: §3 · p. 9

Lowering the barrier—and the affective payoff

• Small, self-contained examples may lower the tooling barrier, while the encouraging affective effects are impressions from the authors' courses, not measured effects.The authors report that refuted conjectures and later successful proof attempts seem to encourage open-mindedness, humility, persistence, and may help defuse logic anxiety.Source: §3 · p. 9

4 A Course Walkthrough: The Graded Ladder

• The semester moves from HOL and proof-assistant basics through embedded modal, epistemic, and deontic logics to a capstone; the approach has also been used in other courses, tutorials, and summer schools.The Bamberg course was taught in three successive winter terms to a mixed audience including computer-science and philosophy students.Source: §4 · pp. 9–10
• The course presents an exemplary ladder from puzzles to research-grade arguments, with each transition motivated by a limitation, a need for modelling resources, or a new application.Instructors may enter, leave, or branch at any rung rather than follow a prescribed curriculum.Source: §4 · pp. 9, 11

4.1 Rung 1—A logic puzzle, and its limits

• The opening puzzle lets students use machine feedback to find consistent configurations, then exposes how truth-functional readings of “says” and “knows” make any two truths interchangeable.The two surviving configurations are that both children tell the truth or both lie.Source: §4.1 · p. 12, Figure 4 · p. 12, Figure 5 · p. 13

4.2 Rung 2—Modal logic, and the modal-logic cube

• Modal logic repairs the truth-functional collapse by making propositions world-dependent, while the modal-logic cube lets students test frame conditions and machine-check proofs or countermodels.The modal repair leaves logical omniscience intact, and static modal logic cannot represent announcement updates, motivating further logics.Source: §4.2 · pp. 13–14

4.3 An epistemic sequel: the Wise Men

• After two public “I do not know” announcements, the Wise Men theorem establishes that the third man knows his spot is white; automated provers verify it and Nitpick traces the remaining possibilities.The same machinery also handles puzzle variants by proof or countermodel.Source: §4.3 · pp. 14–15

Interlude—The virtues of higher-order logic: Boolos’s inference

• f(5,5) steps bound Boolos’s shortest cut-free first-order proof, while higher-order provers dispatch the inference in milliseconds after one inductive-property definition.The required comprehension cut formula is second-order; the supplied higher-order definition lets provers synthesize the remaining lemmas.Source: Interlude—The virtues of higher-order… · p. 16
• HOL is the natural home for semantical embeddings: λ-abstraction lifts connectives to world-dependent functions, and its provers and model finders serve each embedded logic.The proof-search advantage is secondary to this role as the base layer.Source: Interlude—The virtues of higher-order… · p. 16

4.4 Rung 3—Reasoning about norms: Chisholm’s paradox

• F1–F3 do not entail F4: Nitpick finds a model where Jones goes, and the visualiser presents its worlds and deontic accessibility relation as a labelled graph.The graph marks the evaluation world as start and labels every world “go,tell”.Source: §4.4 · p. 17, Figure 7 · p. 17
• In Chisholm’s scenario, SDL’s four renderings fail differently, motivating dyadic systems that interpret conditional obligations through preference relations or contrary-to-duty semantics.WN is inconsistent; WW and NN each create a redundancy, while NW creates both; the Workbench provides encodings of Åqvist’s and Carmo and Jones’s systems.Source: §4.4 · pp. 17–18

4.5 Rung 4—Gödel’s ontological argument

• Scott’s variant encodes Gödel’s argument with one primitive, three definitions, and five axioms; provers derive necessary existence while Nitpick finds a model of the axioms.The primitive is positive property, and the definitions include God-likeness, essence, and necessary existence.Source: §4.5 · p. 18
• Gödel’s original axioms are inconsistent already in base logic K, whereas the final theorem in Scott’s variant requires a symmetric accessibility relation.The original inconsistency yields everything; the machine refutation has a human-readable reconstruction through an empty-essence lemma [30].Source: §4.5 · pp. 18–19
• The capstone connects classroom tools to research: students can interrogate a formalised metaphysical argument, and projects can extend the ladder into published research.Examples include a public-announcement embedding published in the Journal of Logic and Computation and entered into the Archive of Formal Proofs.Source: §4.5 · p. 19

• Sledgehammer searches for proofs and Nitpick for counterexamples, giving students something to inspect whether a statement is true or false.Isabelle’s try command can invoke both tools at once.Source: §5 · pp. 19–20
• The LogiKEy visualiser turns Nitpick’s textual models into labelled graphs of worlds, valuations, and accessibility or preference edges.It addresses the difficulty of reading large models and unfamiliar function-update notation, and prepares graphs for slides or papers.Source: §5 · p. 20, Figure 9 · p. 20
• Automated assessment checks uploaded Isabelle proofs against a specification and can return a verdict within minutes, with unsuccessful attempts retained and annotated.Coupling Isabelle with DOMjudge has supported larger deployments; in class, checking sustains a rapid conjecture–attempt–feedback loop.Source: §5 · p. 20
• Language models can draft formalisations from natural-language descriptions, but students must still judge whether the definitions and assumptions capture the intended meaning.Sledgehammer and Nitpick test whether a draft proves the intended result or admits an unintended countermodel; the approach also raises assignment-outsourcing concerns.Source: §5 · pp. 20–21
• Using a general-purpose research proof assistant buys power and continuity with research practice at the price of a steeper initial interface.This is the stated trade-off against a purpose-built teaching applet.Source: §5 · p. 21

What we observed

• Across three Bamberg course runs, exploration engaged students across disciplines, and mixed groups often complemented one another’s tool fluency and grasp of philosophical stakes.Recurring hurdles included Isabelle syntax, understanding Sledgehammer proofs, and installation on heterogeneous laptops; small editable examples helped.Source: §6 · p. 21
• Machine checking supported open-ended assignments and let students’ questions about work-in-progress theories uncover issues that led to corrected definitions or added premises.The capstone also gave earlier material a visible purpose, according to the authors’ classroom observations.Source: §6 · p. 21

Relation to other tool-based approaches

• Unlike tools that fix one logic or calculus, LogiKEy embeds the semantics of many logics in a general-purpose research proof assistant, exchanging repeated ad-hoc formalisation costs for reusable infrastructure.The authors describe the trade as an exchange, not elimination, of formal overhead; a purpose-built tutor can serve as a first encounter, with LogiKEy as a follow-up for students who want to go further.Source: §6 · pp. 22–23

7 Conclusion and Outlook

• A single expressive meta-logic in a proof assistant supports a mixed cohort learning many logics uniformly and experimentally, with machine-checked work.The chapter illustrates this claim with a graded ladder of classroom examples and supporting tools.Source: §7 · p. 23
• The chapter's formal results are machine-checked and reproducible, but claims about mixed-cohort teaching and student engagement rest on the authors' experience.Whether the approach improves skills, changes barriers for particular groups, compares with purpose-built tutors, or supports learning assessment with language models remains open.Source: §7 · p. 23
• Future directions include language-model assistance with formalisation and richer interactive and visual tools for exploring Kripke models.The chapter specifically points to extending the visualiser of.Source: §7 · p. 23
• The LogiKEy approach is not tied to Isabelle: proof assistants whose logic extends higher-order logic can host the same semantical embeddings.A Lean 4 port of the ontological-argument material reproduces the embeddings, definitions, and theorems; portability can let courses use students' existing proof assistant.Source: §7 · p. 23
• Machine-checked embedding work reaching monadic second-order logic and verified deep embeddings of HOL provides scope for graduate-level metatheory.A growing library of openly available verified developments also gives instructors ready-made material at different teaching levels.Source: §7 · pp. 23–24
• The platform's research on normative and epistemic reasoning points toward extending the approach to teaching AI ethics.The course materials are openly available for others to adapt.Source: §7 · p. 24