Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Teaching Higher-Order Logic Using Isabelle

Simon Tobias Lund, Jørgen Villadsen

TL;DR

The paper introduces a compact, readable formalization of higher-order logic in Isabelle/Pure as a teaching tool, offering an approachable path to Isabelle/HOL without heavy automation. It presents three interrelated formalisms—FOL_Implicational_Axiomatics.thy, FOL_Natural_Deduction.thy, and HOL_Pure.thy—built on Pure and Deep Embedding techniques to illustrate propositional, first-order, and higher-order reasoning, including intuitionistic and classical variants. Through sample natural deduction proofs (propositional, first-order, and Cantor’s theorem in HOL_Pure) and systematic comparisons between implicational axiomatics and natural deduction, the work demonstrates how to teach logic progressively while preserving logical rigor. The approach has been deployed in coursework since 2020, with positive educational outcomes and online availability, underscoring its practical impact for teaching formal reasoning and the foundations of mathematics in proof assistants. The framework also clarifies the relationships between Pure-based formalisms and the standard Isabelle/HOL ecosystem, enabling students to transition to more automated systems while understanding the underlying logic.

Abstract

We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good introduction for someone looking into learning about higher-order logic and proof assistants, without having to study the much more complex Isabelle/HOL with heavier automation. To showcase our development and approach we explain a sample proof, describe the axioms and rules of our higher-order logic, and discuss our experience with teaching the subject in a classroom setting.

Teaching Higher-Order Logic Using Isabelle

TL;DR

The paper introduces a compact, readable formalization of higher-order logic in Isabelle/Pure as a teaching tool, offering an approachable path to Isabelle/HOL without heavy automation. It presents three interrelated formalisms—FOL_Implicational_Axiomatics.thy, FOL_Natural_Deduction.thy, and HOL_Pure.thy—built on Pure and Deep Embedding techniques to illustrate propositional, first-order, and higher-order reasoning, including intuitionistic and classical variants. Through sample natural deduction proofs (propositional, first-order, and Cantor’s theorem in HOL_Pure) and systematic comparisons between implicational axiomatics and natural deduction, the work demonstrates how to teach logic progressively while preserving logical rigor. The approach has been deployed in coursework since 2020, with positive educational outcomes and online availability, underscoring its practical impact for teaching formal reasoning and the foundations of mathematics in proof assistants. The framework also clarifies the relationships between Pure-based formalisms and the standard Isabelle/HOL ecosystem, enabling students to transition to more automated systems while understanding the underlying logic.

Abstract

We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good introduction for someone looking into learning about higher-order logic and proof assistants, without having to study the much more complex Isabelle/HOL with heavier automation. To showcase our development and approach we explain a sample proof, describe the axioms and rules of our higher-order logic, and discuss our experience with teaching the subject in a classroom setting.
Paper Structure (15 sections, 1 figure)

This paper contains 15 sections, 1 figure.

Table of Contents

  1. Introduction
  2. Approach and Contributions
  3. Related Work
  4. Sample Natural Deduction Proofs in Isabelle
  5. Propositional Logic
  6. First-Order Logic
  7. Higher-Order Logic
  8. First-Order Logic --- Soundness and Completeness
  9. Implicational Axiomatics
  10. Natural Deduction
  11. Comparison of Implicational Axiomatics and Natural Deduction
  12. Higher-Order Logic --- Intuitionistic Logic
  13. Higher-Order Logic --- Classical Logic
  14. Further Developments and Concluding Remarks
  15. Acknowledgements

Figures (1)

  • Figure 1: The formalization of implicational axiomatics for first-order logic (the first 7 axioms and rules) and the formalization of natural deduction for first-order logic (the last 7 rules).