Isabelle/HOL as a Meta-Language for Teaching Logic

TL;DR

This paper demonstrates how Isabelle/HOL can be effectively used as a meta-language for teaching logic through three formalizations, enhancing logic education with formal tools and interactive proof systems.

Contribution

It introduces three formalizations in Isabelle/HOL tailored for teaching logic, showcasing their educational benefits and practical implementation in a course on automated reasoning.

Findings

Formalizations support logic teaching effectively

Interactive proof tools enhance student understanding

Reflections suggest future improvements in logic education

Abstract

Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of classical propositional logic with only two primitive symbols), the second is the Natural Deduction Assistant (NaDeA), and the third is a one-sided sequent calculus that uses our Sequent Calculus Verifier (SeCaV). We describe each formalization in turn, concentrating on how we used them in our teaching, and commenting on features that are interesting or useful from a logic education perspective. In the conclusion, we reflect on the lessons learned and where they might lead us next.