Proof-theoretic Conservativity for HOL with Ad-hoc Overloading

• 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.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

NATURVETENSKAP  -- Matematik -- Algebra och logik (hsv//swe)

NATURAL SCIENCES  -- Mathematics -- Algebra and Logic (hsv//eng)

Nyckelord

Classical higher-order logic

Conservative theory extension

Proof-theoretic conservativity

Ad-hoc overloading

Isabelle

Computer Science

Datavetenskap

Publikations- och innehållstyp

ref (ämneskategori)

kon (ämneskategori)