*To*: Rob Arthan <rda at lemma-one.com>*Subject*: [isabelle] conservativity of HOL constant and type definitions*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Mon, 24 Oct 2016 18:16:48 +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>, HOL-info list <hol-info at lists.sourceforge.net>*In-reply-to*: <AM3PR01MB1313BE012FC7B906B4F698C9B7A90@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>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSLiLJtyO6LAY21kypBHYOCN/12g==*Thread-topic*: conservativity of HOL constant and type definitions

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

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

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

- Previous by Date: Re: [isabelle] Output panel term printing
- Next by Date: Re: [isabelle] conservativity of HOL constant and type definitions
- Previous by Thread: Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- 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