*To*: OndÅej KunÄar <kuncar at in.tum.de>*Subject*: Re: [isabelle] conservativity of HOL constant and type definitions*From*: Rob Arthan <rda at lemma-one.com>*Date*: Mon, 24 Oct 2016 21:37:00 +0100*Cc*: "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>, Andrei Popescu <A.Popescu at mdx.ac.uk>, HOL-info list <hol-info at lists.sourceforge.net>*In-reply-to*: <d54914d2-dc95-92b9-769f-1c20c03a0526@in.tum.de>*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> <E8B13090-D8D7-42DB-ACD0-72F074D0CA45@lemma-one.com> <d54914d2-dc95-92b9-769f-1c20c03a0526@in.tum.de>

Ondrej, > On 24 Oct 2016, at 20:32, OndÅej KunÄar <kuncar at in.tum.de> wrote: > > On 10/24/2016 09:16 PM, Rob Arthan wrote: >> 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 made that sound too strong: I was just making a conjecture: for "think" read "feel". > They could. You can try to argue by "unfolding" the type definitions. "Unfolding" of types is exactly what I had in mind when I mentioned the methods used in connect with Heyting arithmetic. > Again, the model-theoretic conservativity is stronger than the proof-theoretic in general. And here you don't have an existential quantifier for type constructors so you [can't] use the approach as you did for constants. Yes, but if the unfolding approach works, you would have reduced the essential properties of the type definition to a statement about the existence of a certain subset of the representation type bearing a relationship with some siubsets of the parameter types and you would then be able to deduce model-theoretic conservativeness. That's why I felt, that if Andrei is right that the type definition principle is not model-theoretically conservative w.r.t. Henkin models (his point (2.2)), then it won't be proof-theoretically conservative either, because the unfolding argument must break down somewhere. It would be very useful to see an example of a type definition that is not conservative w.r.t. Henkin models. Regards, Rob.

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

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

**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

**Re: [isabelle] conservativity of HOL constant and type definitions***From:*Rob Arthan

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

- Previous by Date: Re: [isabelle] conservativity of HOL constant and type definitions
- Next by Date: Re: [isabelle] conservativity of HOL constant and type definitions
- Previous by Thread: Re: [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