*To*: Rob Arthan <rda at lemma-one.com>*Subject*: 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 <A.Popescu at mdx.ac.uk>*Date*: Mon, 24 Oct 2016 10:02:44 +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*: <B9568E67-6613-409D-8278-6E87BA2448AC@lemma-one.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>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSLFObGeV9wB/79UOAPLP08G8x3qC01loAgAEQtICAACDnyIAAkAOAgADDboA=*Thread-topic*: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

Hi Rob, >> As discussed off-list with you and Ondrej, the case covered by new_specification or gen_new_specification is one where (B) implies (A). Indeed. Many thanks (to you and Roger) for the clarifications. >> Of course, none of the above works for an extension that introduces new types. Your paper is a very nice contribution to the problem of defining new types. Thanks. Also, thanks for bringing up new_specification and gen_new_specification. After having a closer look at them, I see that the definitional dependency analysis we introduce in the paper can be easily extended to cope with these mechanisms -- which means that they don't raise additional difficulties in the delicate balance between constant overloading and typedef, and therefore are in principle suitable for Isabelle/HOL. We'll add a discussion of this in the journal version (and point you to it when it's available). Best, Andrei ________________________________ From: Rob Arthan <rda at lemma-one.com> Sent: 23 October 2016 22:56 To: Andrei Popescu Cc: 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: Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)? Andrei, > On 23 Oct 2016, at 14:31, Andrei Popescu <A.Popescu at mdx.ac.uk> wrote: > > Hi Rob, > > >> It's the other way round. Soundness implies that proof-theoretic conservativity implies model-theoretic conservativity. > > Ondra's statement was the correct one. > > Let's spell this out, to make sure we are speaking of the same thing. Say you have a signature Sigma' extending a signature Sigma (by adding some constant and type constructor symbols). Then every Sigma'-model M' produces a Sigma-Model, Forget(M'), by forgetting the interpretation of the symbols in Sigma' minus Sigma. Moreover, > > (*) For every closed Sigma-formula phi, we have that M |= phi holds iff Forget(M) |= phi holds. > > Let T be a Sigma-theory (i.e., a set of closed Sigma-formulas), and let T' be a Sigma'-theory that includes T. > T' is called: > > (A) a model-theoretic conservative extension of T if, for all Sigma-models M of T, there exists a Sigma'-model M' of T' such that Forget(M') = M. > > (B) a proof-theoretic conservative extension of T if, for all closed Sigma-formulas phi, T' |- phi implies T |- phi. > > Assuming soundness *and completeness*, we have (A) implies (B). Proof: We can reason about semantic deduction |= instead of syntactic deduction. Assume T'|= phi .To prove T|= phi, let M |= T; by (A), we find M' |= T' such that Forget(M') = M. With T'|= phi, we obtain Forget(M')|= phi. From this and (*), we obtain M' |= phi, as desired. > > In general, (B) does not imply (A), and I don't know of interesting sufficient conditions for when it does. As discussed off-list with you and Ondrej, the case covered by new_specification or gen_new_specification is one where (B) implies (A). The interesting sufficient conditions that apply are; (1) T' is a finitely axiomatizable expansion of T introducing finitely many new constants and no new types and (2) the logical language admits an existential quantifier with the usual proof rules and semantics. For then if T' satisfies (B), let phi(x_1, ... x_n) denote the result of taking the conjunction of the formulas that axiomatize T' and replacing the new constants c_1, ..., c_n by variables x_1, ..., x_n. Then T' proves psi ::= exists x_1, ... , x_n. phi(x_1, ..., x_n). By (B), T proves psi, but then, by soundness, psi holds in every model of T, which implies (A). Of course, none of the above works for an extension that introduces new types. Your paper is a very nice contribution to the problem of defining new types. Regards, Rob.

**Follow-Ups**:**[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

- Previous by Date: Re: [isabelle] polymorphic enough friend
- Next by Date: [isabelle] Output panel term printing
- 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: [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