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
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
