Isabelle's Metalogic: Formalization and Proof Checker

TL;DR

This paper formalizes Isabelle's metalogic and proof terms within Isabelle/HOL, develops an executable proof checker, and verifies the correctness of proofs across various logics and theories.

Contribution

It introduces a formalization of Isabelle's metalogic and proof checker, ensuring correctness and integration within the Isabelle environment.

Findings

Proof checker is correct with respect to the metalogic

Successfully checked proofs across multiple logics and theories

Formalization enhances reliability of Isabelle proofs

Abstract

Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.