Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

TL;DR

This paper presents a formalization of intuitionistic and classical propositional logic in Isabelle/Pure, emphasizing a logical framework approach that enhances teaching and understanding of logic in automated reasoning courses.

Contribution

It introduces a logical framework modeling approach for propositional logic in Isabelle, improving pedagogical clarity over previous deep embedding methods.

Findings

Effective in teaching logic concepts in automated reasoning courses

Simplifies logical formalization with natural deduction in Isabelle

Enhances pedagogical outcomes compared to earlier approaches

Abstract

We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.