Arve Gengelbach, Johannes Åman Pohjola, and Tjark Weber. In Claudio Sacerdoti Coen and Alwen Tiu, editors, Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020, volume 332 of EPTCS, pages 1-17, 2020.
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.
@inproceedings{gengelbach20mechanisation,
author = {Arve Gengelbach and Johannes {\AA}man Pohjola and Tjark Weber},
title = {Mechanisation of Model-theoretic Conservative Extension for {HOL} with Ad-hoc Overloading},
editor = {Claudio Sacerdoti Coen and Alwen Tiu},
booktitle = {Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2020, Paris, France, 29th June 2020},
volume = {332},
series = {{EPTCS}},
pages = {1--17},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.332.1},
doi = {10.4204/EPTCS.332.1}
}