[isabelle] conservativity of HOL constant and type definitions



Since the conservativity topic has been touched upon, I would like to summarize the situation in HOL as I understand it now, after our discussion.
(Myself, I am mainly interested in Isabelle/HOL, but this is an important related problem.)
Please, correct me if and where I am wrong.

(1) The constant definition mechanisms (including the more general ones) are known to be:
(1.1) model-theoretic conservative w.r.t. standard (Pitts) models
(1.2) model-theoretic conservative w.r.t. Henkin models
(1.3) proof-theoretic conservative

(2) The type definition mechanism is known to be:
(2.1) model-theoretic conservative w.r.t. standard models
(2.2) *not* model-theoretic conservative w.r.t. Henkin models (by an easy counterexample -- a Henkin model that does not have the right infrastructure to support a given typedef)

Concerning proof-theoretic conservativity of type definitions: there does not exist any proof of this -- or does it? It certainly doesn't follow from (2.1).

Best,
  Andrei



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.