Arve Gengelbach and Tjark Weber. In Violet Ka I Pun, Volker Stolz, and Adenilso Simão, editors, Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings, volume 12545 of Lecture Notes in Computer Science, pages 23-42. Springer, 2020.
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.
@inproceedings{gengelbach20proof,
author = {Arve Gengelbach and Tjark Weber},
title = {Proof-Theoretic Conservative Extension of {HOL} with Ad-hoc Overloading},
editor = {Violet Ka I Pun and Volker Stolz and Adenilso Sim{\~{a}}o},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings},
volume = {12545},
series = {Lecture Notes in Computer Science},
pages = {23--42},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-64276-1\_2},
doi = {10.1007/978-3-030-64276-1\_2}
}