One Metalogic, Many Logics: A Quantitative Pedagogical Framework for Proof-Assistant-Based Logic Teaching with LogiKEy

In the paper's words

Teaching logic to mixed cohorts of computer science, mathematics, and philosophy students is difficult because each cohort brings different expectations and because the standard curriculum fragments into isolated courses on propositional, modal, epistemic, and deontic logic. The LogiKEy methodology addresses this by using classical higher-order logic (HOL) as a universal metalogic: object logics are encoded as semantical embeddings inside a single proof assistant such as Isabelle/HOL, so that students learn, experiment with, and compare logics in one environment. This paper complements the qualitative, example-driven curriculum design of LogiKEy with explicit combinatorial analysis of its graded example sequence — liars-and-truth-tellers puzzles, the Wise Men puzzle, Boolos's curious inference, Chisholm's paradox, and Gödel's ontological argument. [...]

The abstract, verbatim, and its opening sentence is the claim. Every line below is quoted from the text.

Numbers it reports

1. The model-size trajectory is: $$8 \to 7 \to 6 \to 4$$ and the information gain of the two ignorance announcements is a reduction from $7$ to $4$ candidate worlds, i.e. a shrinkage factor of $7/4 = 1.75$.

   from 4.3 Stage 3: The Wise Men puzzle — model dynamics under public announcement

2. If the six stages of Section 3 are allocated in the ratio $2 : 3 : 3 : 4 : 4 : 4$ (reflecting increasing sophistication, per the graded sequence [1], [2]), the total ratio weight is $2 + 3 + 3 + 4 + 4 + 4 = 20$, so each weight unit is $$\frac{28}{20} = 1.4 \text{ hours},$$ and the stage allocations are $2 \times 1.4 = 2.8$, $3 \times 1.4 = 4.2$, $3 \times 1.4 = 4.2$, $4 \times 1.4 = 5.6$, $4 \times 1.4 = 5.6$, and $4 \times 1.4 = 5.6$ hours respectively.

   from 4.7 Course-time projection (labeled projection)

3. The Wise Men factual model follows the trajectory $8 \to 7 \to 6 \to 4$ under the king's announcement and two ignorance announcements, a shrinkage factor of $7/4 = 1.75$ from the first announcement onward; a DEL action model with $|E| = 3$ events over the original $8$ worlds yields $8 \times 3 = 24$ worlds (Section 4.3).

   from 5. Results

4. Under the stated assumptions of Section 4.7 ($28$ contact hours, allocation ratio $2:3:3:4:4:4$), the six stages receive $2.8$, $4.2$, $4.2$, $5.6$, $5.6$, and $5.6$ hours respectively; uncertainty is dominated by the assumed ratio, which we have not validated empirically.

   from 5. Results

5. R2: the modal upgrade expands the student's search space from $8$ to $\approx 1.84 \times 10^{19}$, a factor of $$\frac{2^{64}}{2^3} = 2^{61} \approx 2.31 \times 10^{18}$$ (checked: $ 2^{61} = 2{,}305{

   from 5. Results

How it is done

1. The LogiKEy methodology addresses this by using classical higher-order logic (HOL) as a universal metalogic: object logics are encoded as semantical embeddings inside a single proof assistant such as Isabelle/HOL, so that students learn, experiment with, and compare logics in one environment.

   from Abstract

2. Through such semantical embeddings, one proof assistant (e.g.

   from 1. Introduction

3. The LogiKEy methodology itself is presented in [1] and [2], which report more than a decade of use in courses, summer schools, and tutorials. [1] makes the pedagogical case for proof assistants in the logic classroom and presents the graded sequence of examples from the liars-and-truth-tellers puzzle through Gödel's ontological argument; [2] is the full paper elaborating the same program, including the rebuttal that embedding everything in classical HOL is pluralism rather than monism, since the object logics remain genuinely distinct — their theorems, valid inferences, and counter-models differ — even though their semantics are uniformly definable in HOL.

   from 2. Background and Related Work

4. None of this requires new tooling: each definition is a HOL constant, each metatheorem a HOL theorem, each counter-model a HOL-computable structure.

   from 3.1 Semantical embeddings in HOL

What would falsify it

1. We argue that these computed checkpoints, rather than anecdote, are what make each curricular transition pedagogically forced, and we identify failure modes, falsification conditions, and open questions for empirical validation.

   from Abstract

2. We derive these numbers with full arithmetic in Section 4, report them in Section 5, and use them in Section 6 to defend the pluralism claim and to state falsification conditions.

   from 1. Introduction

Where the claim stops

1. We further derive a labeled projection for course-time allocation under stated assumptions.

   from Abstract

2. A logic classroom with only computer science students can assume comfort with formalism and an interest in verification; a classroom with only philosophy students can assume interest in argument analysis but not in type theory.

   from 1. Introduction

3. The LogiKEy papers present a graded sequence of classroom examples, each transition motivated by a limitation of the preceding representation: 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 metalogic buys even for automated proof search; Chisholm's paradox moves into deontic logic and then dyadic deontic logic; and Gödel's ontological argument reaches research-level metaphysics [1], [2].

   from 1. Introduction

Where to read

1. Abstract219 words · 1 min
2. 1. Introduction490 words · 2 min
3. 2. Background and Related Work762 words · 3 min
4. 3. Methods329 words · 1 min
5. 4. Analysis1,637 words · 7 min
6. 5. Results351 words · 2 min