Comprehending Isabelle/HOL’s Consistency
Ondřej Kunčar and Andrei Popescu
Abstract. The proof assistant Isabelle/HOL is based on an extension of
Higher-Order Logic (HOL) with ad hoc overloading of constants. It turns out that the
interaction between the standard HOL type definitions and the Isabelle-specific
ad hoc overloading is problematic for the logical consistency. In previous work,
we have argued that standard HOL semantics is no longer appropriate for capturing
this interaction, and have provided consistency using a non-standard semantics.
That proof was rather intricate and exotic, making it harder to digest by the
Isabelle/HOL community. In this paper, we prove consistency by proof-theoretic
means—following the healthy intuition of definitions as abbreviations, realized in
HOLC, a logic that augments HOL with comprehension types. We hope that our
new proof settles the Isabelle/HOL consistency problem once and for all. In addition,
HOLC offers a framework for justifying the consistency of new deduction
schemas that address practical user needs.
Full text available here.