Andrei, > On 24 Oct 2016, at 19:16, Andrei Popescu <a.pope...@mdx.ac.uk> wrote: > > 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
I agree with all of the above. > (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) > I don't see how to construct a counterexample. Could you give some more details, please. > 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). I am pretty sure nothing has been published and, if you are right about (2.2), then I don't think type definitions can be proof-theoretically conservative. I have had thoughts about how one might prove that type definitions are conservative by using relativisation tricks like the ones that are used to prove that Heyting arithmetic over finite types is conservative over first-order Heyting arithmetic. I think this problem may well be sensitive to the choice of non-logical axioms: e.g., it is possible that type definitions aren't conservative over an intuitionistic fragment of HOL but are conservative over HOL with AC. Regards, Rob. ------------------------------------------------------------------------------ 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
