*To*: Rob Arthan <rda at lemma-one.com>, Ondřej Kunčar <kuncar at in.tum.de>*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*: Sun, 23 Oct 2016 13:31:07 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*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>, Ken Kubota <mail at kenkubota.de>, HOL-info list <hol-info at lists.sourceforge.net>*In-reply-to*: <5B8D62CD-0391-47FA-AD1F-52F52A0B3F2C@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>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSLFObGeV9wB/79UOAPLP08G8x3qC01loAgAEQtICAACDnyA==*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, >> 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. Best, Andrei ________________________________ From: Rob Arthan <rda at lemma-one.com> Sent: 23 October 2016 12:23 To: Ondřej Kunčar Cc: Ken Kubota; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-users at lists.cam.ac.uk; Roger Bishop Jones; Prof. Peter B. Andrews; Andrei Popescu; 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)? Ondrej, > On 22 Oct 2016, at 20:07, Ondřej Kunčar <kuncar at in.tum.de> wrote: > > Hi Rob, > you are right that we mention only the plain definitions in HOL and not > the implicit ones, when we compare the definitional mechanism of HOL and > Isabelle/HOL. (If this what you meant; I assume you didn't mean to say > that the overloading in Isabelle is 25 years out of date). No. I was just referring to new_specification. > I clearly remember that one of the early versions of our paper contained > the comment that the current HOL provers use the more powerful mechanism > that you mentioned but I guess that it was lost during later editing. We > will include it again into the journal version of the paper. > Thanks. I’m glad I raised my comment in time for you to do that. > I wanted to comment on your statement that A. Pitts proved that > definitions in HOL are conservative. Such statements are always a little > bit puzzling to me because when you say conservative (without any > modifier), I always think that you mean the notion that "nothing new can > be proved if you extend your theory (by a definition)". I think a lot of > people (including me) think that this is THE conservativity. There is > also a notion of the model-theoretic conservativity that requires that > every model of the old theory can be expanded to a model of the new > theory. This is a stronger notion and implies the proof conservativity. > It’s the other way round. Soundness implies that proof-theoretic conservativity implies model-theoretic conservativity. In the absence of completeness, an x with some property phi(x) might exist in every model, but you might not be able to prove that. Taking phi(c) as the defining property of a new constant c would then be conservative model-theoretically but not proof-theoretically. > As far as I know, A. Pitts considers only a subset of all possible > models (so called standard models) in his proof and he only proves that > these models can be extended from the old to the new theory. But as far > as I know this does not imply the proof conservativity. Andy Pitts gives a proof of the model-theoretic conservativity of new_specification with respect to standard models. You are quite right that in the absence of completeness this is a weaker result than proof-theoretic completeness. I don’t think it’s difficult to extend the result to general models (Henkin models) and so get proof-theoretic conservativity. I suspect Andy just didn’t want to introduce a lot of extra technical detail. I proved proof-theoretic conservativity for the new mechanism gen_new_specification. As new_specification is derivable using gen_new_specification, this gives you proof-theoretic conservativity for both. (Thanks to Scott for correcting my statement about what has been formalised so far in HOL4). Regards, Rob.

**Follow-Ups**:

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

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