# zbMATH — the first resource for mathematics

From types to sets by local type definition in higher-order logic. (English) Zbl 07024458
Summary: Types in higher-order logic (HOL) are naturally interpreted as nonempty sets. This intuition is reflected in the type definition rule for the HOL-based systems (including Isabelle/HOL), where a new type can be defined whenever a nonempty set is exhibited. However, in HOL this definition mechanism cannot be applied inside proof contexts. We propose a more expressive type definition rule that addresses the limitation and we prove its consistency. This higher expressive power opens the opportunity for a HOL tool that relativizes type-based statements to more flexible set-based variants in a principled way. We also address particularities of Isabelle/HOL and show how to perform the relativization in the presence of type classes.

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: