*To*: Andrei Popescu <A.Popescu at mdx.ac.uk>*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*: Rob Arthan <rda at lemma-one.com>*Date*: Sun, 23 Oct 2016 22:56:31 +0100*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*: <HE1PR01MB1321BAD7F561972B00688168B7D60@HE1PR01MB1321.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>

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

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

- 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: [isabelle] The HOL family, HOL Light, Q0, and type abstraction
- 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