*To*: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>*Subject*: Re: [isabelle] [Hol-info] conservativity of HOL constant and type definitions*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Tue, 25 Oct 2016 08:36:56 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*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>, Rob Arthan <rda at lemma-one.com>, HOL-info list <hol-info at lists.sourceforge.net>*In-reply-to*: <CAMej=25R6sJSsFHP_=D3kNQXNYtv3epuopUK6xXAQHtCA2T4Qg@mail.gmail.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> <E8B13090-D8D7-42DB-ACD0-72F074D0CA45@lemma-one.com> <d54914d2-dc95-92b9-769f-1c20c03a0526@in.tum.de> <119AB613-C64E-4D78-B31B-619D8862635D@lemma-one.com> <AM3PR01MB1313EB00391C035A0ED376FBB7A90@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>, <CAMej=25R6sJSsFHP_=D3kNQXNYtv3epuopUK6xXAQHtCA2T4Qg@mail.gmail.com>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSLprybf7PV8Po1UORO1JQUVUERA==*Thread-topic*: [Hol-info] conservativity of HOL constant and type definitions

Hi Ramana, Thanks for the confirmation (and for the pointer). Yes, the base theories in your formalized result do qualify as arbitrary in my terminology. :-) I assume "arbitrary theories" include the usual signature and axioms of polymorphic classical higher order logic with equality, Infinity and Choice. Your result is more general. Andrei ________________________________ From: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> Sent: 25 October 2016 08:24 To: Andrei Popescu Cc: Rob Arthan; Ondřej Kunčar; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-users at lists.cam.ac.uk; Roger Bishop Jones; Prof. Peter B. Andrews; HOL-info list Subject: [SPAM: 10.600] Re: [Hol-info] conservativity of HOL constant and type definitions Just to answer the question-mark in (2.1), I mechanised a proof that new_type_definition is model-theoretically conservative for standard models and arbitrary base theories. To be clear, the proof assumes the base theory contains "fun", "bool", and "=", and that it has a model that interprets these types/constants in the standard way. I presume this counts as "arbitrary", but maybe it doesn't :) (The proof is at https://github.com/CakeML/cakeml/blob/master/candle/standard/semantics/holExtensionScript.sml#L366.) On 25 October 2016 at 09:06, Andrei Popescu <A.Popescu at mdx.ac.uk<mailto:A.Popescu at mdx.ac.uk>> wrote: The counterexample I had in mind is due to Makarius Wenzel (https://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf, page 8): The theory T containing the single HOL formula "no type has cardinal 3" has a Henkin model M; yet, M has no expansion to the theory T extended with the definition of the type {1,2,3}. But actually this extension is not proof-theoretically conservative either (as it even breaks consistency) ... In fact, now I see that I have not clearly spelled out all the assumptions of the statements in my summary. So let me try again, also factoring in the base (i.e., to-be-extended) theory: (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 and arbitrary base theories (1.2) model-theoretic conservative w.r.t. Henkin models and arbitrary base theories (1.3) proof-theoretic conservative and arbitrary base theories (2) The type definition mechanism is known to be: (2.1) model-theoretic conservative w.r.t. standard models and arbitrary(?) base theories and known *not* to be: (2.2) model-theoretic conservative w.r.t. Henkin models and arbitrary base theories (2.3) proof-theoretic conservative w.r.t. Henkin models and arbitrary base theories On the other hand, it is of course legitimate to lower the expectation for typedefs, so we could ask what happens with (2.2) and (2.3) if we restrict to base theories that are themselves definitional. Here, the above counterexample does not work. And yes, Rob, without being able to follow your Heyting arithmetic analogy, I do see the similarity between a possible semantic proof of definitional-base-(2.2) and a possible syntactic proof of definitional-base-(2.3) (both revolving around the notion of relativization to sets). But I am surprised that a lot of attention has been given to the conservativity of constant definitions/specifications, but not to that of the old and venerable typedef. Best, Andrei ________________________________ From: Rob Arthan <rda at lemma-one.com<mailto:rda at lemma-one.com>> Sent: 24 October 2016 21:37 To: Ondřej Kunčar Cc: Andrei Popescu; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-users at lists.cam.ac.uk<mailto:cl-isabelle-users at lists.cam.ac.uk>; Roger Bishop Jones; Prof. Peter B. Andrews; HOL-info list Subject: Re: conservativity of HOL constant and type definitions Ondrej, > On 24 Oct 2016, at 20:32, Ondřej Kunčar <kuncar at in.tum.de<mailto: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. ------------------------------------------------------------------------------ The Command Line: Reinvented for Modern Developers Did the resurgence of CLI tooling catch you by surprise? Reconnect with the command line and become more productive. Learn the new .NET and ASP.NET<http://ASP.NET> CLI. Get your free copy! http://sdm.link/telerik _______________________________________________ hol-info mailing list hol-info at lists.sourceforge.net<mailto:hol-info at lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info

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

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

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

- Previous by Date: Re: [isabelle] Isabelle2016-RC0: cvc4 crashing
- Next by Date: Re: [isabelle] Isabelle2016-1-RC0 available for testing
- Previous by Thread: Re: [isabelle] conservativity of HOL constant and type definitions
- Next by Thread: Re: [isabelle] Isabelle2016-RC0 - text with cartouches outside theory
- 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