Model-theoretic conservative extension for definitional theories

DOI10.1016/j.entcs.2018.10.009zbMath1434.03028OpenAlexW2898891135WikidataQ113317506 ScholiaQ113317506MaRDI QIDQ2333319

Arve Gengelbach, Tjark Weber

Publication date: 12 November 2019

Full work available at URL: https://doi.org/10.1016/j.entcs.2018.10.009

zbMATH Keywords

Isabelleclassical higher-order logicconservative theory extensiondefinitional theoriesground semanticsmodel-theoretic conservativity

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Basic properties of first-order languages and structures (03C07) Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isabelle
• Isabelle/HOL
• ETPS

Cites Work

• Unnamed Item
• On definitions of constants and types in HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• An introduction to mathematical logic and type theory: To truth through proof.
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• HOL Constant Definition Done Right
• A Consistent Foundation for Isabelle/HOL
• Comprehending Isabelle/HOL’s Consistency
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic

This page was built for publication: Model-theoretic conservative extension for definitional theories