Model-Theoretic Conservative Extension for Definitional Theories

Arve Gengelbach and Tjark Weber. In Sandra Alves and Renata Wasserman, editors, 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017, volume 338 of Electronic Notes in Theoretical Computer Science, pages 133-145. Elsevier, 2017.

Abstract

Many logical frameworks allow extensions, i.e. the introduction of new symbols, by definitions. Different from asserting arbitrary non-logical axioms, extensions by definitions are expected to be conservative: they should entail no new theorems in the original language. The popular theorem prover Isabelle implements a variant of higher-order logic that allows ad hoc overloading of constants. In 2015, Kunčar and Popescu introduced definitional theories, which impose a non-circularity condition on constant and type definitions in this logic, and showed that this condition is sufficient for definitional extensions to preserve consistency. We strengthen and generalize this result by showing that extensions of definitional theories are model-theoretic conservative, i.e. every model of the original theory can be expanded to a model of the extended theory.

Download

BibTeX

@inproceedings{gengelbach17model,
  author    = {Arve Gengelbach and Tjark Weber},
  title     = {Model-Theoretic Conservative Extension for Definitional Theories},
  editor    = {Sandra Alves and Renata Wasserman},
  booktitle = {12th Workshop on Logical and Semantic Frameworks, with Applications, {LSFA} 2017, Bras{\'{\i}}lia, Brazil, September 23-24, 2017},
  volume    = {338},
  series    = {Electronic Notes in Theoretical Computer Science},
  pages     = {133--145},
  publisher = {Elsevier},
  year      = {2017},
  url       = {https://doi.org/10.1016/j.entcs.2018.10.009},
  doi       = {10.1016/j.entcs.2018.10.009}
}

Last modified: 2022-01-12