*To*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Subject*: Re: [isabelle] conservativity of HOL constant and type definitions*From*: Rob Arthan <rda at lemma-one.com>*Date*: Mon, 24 Oct 2016 20:16:19 +0100*Cc*: OndÅej KunÄar <kuncar at in.tum.de>, "Prof. Andrew M. Pitts" <Andrew.Pitts at cl.cam.ac.uk>, "Prof. Thomas F. Melham" <thomas.melham at balliol.ox.ac.uk>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>, Roger Bishop Jones <rbj at rbjones.com>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, HOL-info list <hol-info at lists.sourceforge.net>*In-reply-to*: <AM3PR01MB13138EDE9FB883DD33BAB2FDB7A90@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>*References*: <mailman.58165.1476751826.9767.hol-info@lists.sourceforge.net> <ac50a36e-5a5e-a356-6878-a5de00d02282@rbjones.com> <5E3CAC59-87D9-4C98-A58E-1B435A2F1E41@kenkubota.de> <B9CAE32E-026D-4ECB-B0BD-9D69ED2BAC69@lemma-one.com> <64cc1aed-c88f-4084-4ee0-e2981b6b2021@in.tum.de> <5B8D62CD-0391-47FA-AD1F-52F52A0B3F2C@lemma-one.com> <HE1PR01MB1321BAD7F561972B00688168B7D60@HE1PR01MB1321.eurprd01.prod.exchangelabs.com> <B9568E67-6613-409D-8278-6E87BA2448AC@lemma-one.com> <AM3PR01MB1313BE012FC7B906B4F698C9B7A90@AM3PR01MB1313.eurprd01.prod.exchangelabs.com> <AM3PR01MB13138EDE9FB883DD33BAB2FDB7A90@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>

Andrei, > On 24 Oct 2016, at 19:16, Andrei Popescu <A.Popescu at 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.

**Follow-Ups**:**Re: [isabelle] conservativity of HOL constant and type definitions***From:*OndÅej KunÄar

**References**:**[isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Ken Kubota

**Re: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Rob Arthan

**Re: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*OndÅej KunÄar

**Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Rob Arthan

**Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Andrei Popescu

**Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Rob Arthan

*From:*Andrei Popescu

**[isabelle] conservativity of HOL constant and type definitions***From:*Andrei Popescu

- Previous by Date: [isabelle] conservativity of HOL constant and type definitions
- Next by Date: Re: [isabelle] conservativity of HOL constant and type definitions
- Previous by Thread: [isabelle] conservativity of HOL constant and type definitions
- Next by Thread: Re: [isabelle] conservativity of HOL constant and type definitions
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list