Search

Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL main library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover., QC 20220913Part of proceedings: ISBN 978-395977252-5

Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL main library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover.

Safe extension of a logic with definitional axioms need acyclic definitions, because cycles in definitions possibly entail contradiction. In this report we give a mechanised exact characterisation of acyclic overloading definitions. Our results support the soundness argument of the cyclicity checker of the Isabelle/HOL theorem prover, and serve as the theoretical foundation for future verification of such a cyclicity checker.

Logical frameworks are often equipped with an extensional mechanism to define new symbols. The definitional mechanism is expected to be conservative, i.e. it shall not introduce new theorems of the original language. The theorem proving framework Isabelle implements a variant of higher-order logic where constants may be ad-hoc overloaded, allowing a constant to have different definitions for non-overlapping types. In this paper we prove soundness and completeness for the logic of Isabelle/HOL with general (Henkin-style) semantics, and we prove model-theoretic and proof-theoretic conservativity for theories of definitions.

Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions— that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with ad-hoc overloading is consistent. All our results have been formalised in the HOL4 theorem prover.

Many logical frameworks allow extensions, i.e. the introduction of new symbols, by definitions. Different from asserting arbitrary non-logical axioms, extensions by definitions are expected to be conservative: they should entail no new theorems in the original language. The popular theorem prover Isabelle implements a variant of higher-order logic that allows ad hoc overloading of constants. In 2015, Kunčar and Popescu introduced definitional theories, which impose a non-circularity condition on constant and type definitions in this logic, and showed that this condition is sufficient for definitional extensions to preserve consistency. We strengthen and generalize this result by showing that extensions of definitional theories are model-theoretic conservative, i.e. every model of the original theory can be expanded to a model of the extended theory.