Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Abstract
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.
Keywords
Cite
@article{arxiv.2101.03807,
title = {Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading},
author = {Arve Gengelbach and Johannes Åman Pohjola and Tjark Weber},
journal= {arXiv preprint arXiv:2101.03807},
year = {2021}
}
Comments
In Proceedings LFMTP 2020, arXiv:2101.02835