The Foundation of a Generic Theorem Prover

TL;DR

This paper introduces Isabelle, a versatile theorem prover based on higher-order logic, which formalizes various logics and proofs within a unified meta-logic framework, demonstrating soundness, completeness, and practical proof techniques.

Contribution

It presents Isabelle's foundation as a higher-order logic-based meta-logic supporting formalization of multiple logics and proofs, with practical proof techniques and soundness guarantees.

Findings

Axioms for first-order logic are sound and complete.

Backwards proof is formalized via meta-reasoning.

Higher-order logic offers practical advantages over other meta-logics.

Abstract

Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework') in which the object-logics are formalized. Isabelle is now based on higher-order logic -- a precise and well-understood foundation. Examples illustrate use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown sound and complete. Backwards proof is formalized by meta-reasoning about object-level entailment. Higher-order logic has several practical advantages over other meta-logics. Many proof techniques are known, such as Huet's higher-order unification procedure.