Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading

Arve Gengelbach
Johannes Åman Pohjola
Tjark Weber

Definitions of new symbols merely abbreviate expressions in logical frameworks, and no new facts (regarding previously defined symbols) should hold because of a new definition. In Isabelle/HOL, definable symbols are types and constants. The latter may be ad-hoc overloaded, i.e. have different definitions for non-overlapping types. We prove that symbols that are independent of a new definition may keep their interpretation in a model extension. This work revises our earlier notion of model-theoretic conservative extension and generalises an earlier model construction. We obtain consistency of theories of definitions in higher-order logic (HOL) with ad-hoc overloading as a corollary. Our results are mechanised in the HOL4 theorem prover.

In Claudio Sacerdoti Coen and Alwen Tiu: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020), Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 332, pp. 1–17.
Published: 12th January 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.332.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org