I don’t want to put words in Rob’s mouth, as he’s far more knowledgable in this area than I am.
As far as I know, there is no mechanised conservativity proof for HOL’s recent generalised constant specification mechanism. (Here I’m in agreement that “conservativity” without any other modification should refer to the proof theoretic notion, and that’s what I mean here.) Rob certainly has a pencil-and-paper proof. Ramana, Rob, Magnus, and I (although mostly Ramana) proved the soundness of a HOL Light-style logical system, including the generalised constant specification mechanism that Rob refers to (and also designed) and type definition mechanism, with respect to a standard model of higher-order logic. I worked on a mechanised conservativity proof for the definition mechanism for a bit two years ago but got distracted and haven’t returned to it. I think it would be a suitable student project, but I’m not convinced that it’s really that interesting — I wouldn’t be bothered by a sound and consistent definition principle that allowed one to prove more things. Scott > On 2016/10/22, at 20:07, Ondřej Kunčar <kun...@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). > 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. > > 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. > > 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. > > Best, > Ondrej > > On 10/22/2016 12:59 PM, Rob Arthan wrote: >> Ken, >> >> Unfortunately, the paper by Ondrej Kuncar and Andrei Popescu that you cite >> gives >> a description of the definitional mechanisms in HOL that is about 25 years >> out of date. >> The new_specification mechanism allows implicit definitions and cannot be >> viewed >> as a syntactic abbreviation mechanism. There is a proof of the >> conservativeness of a >> (generalisation of) this mechanism in Andy Pitts’ Introduction to the HOL >> Logic (ref. [31] >> in the paper). new_specification is implemented in all the "HOL-based >> provers” listed >> in the paper. >> >> Due to tinkering on my part around 2013, new_specification has been extended >> to relax >> certain constraints on polymorphism that it imposed. The resulting >> gen_new_specification >> has been proved conservative informally by me and formally in HOL4 by Ramana >> Kumar, >> Magnus Myreen and Scott Owens (see their and my papers in ITP 2014 and/or >> JAR 56(3)). >> gen_new_specification is implemented (to my knowledge) in HOL4, ProofPower >> and OpenTheory. >> >> Regards, >> >> Rob. >> >> > > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, SlashDot.org! http://sdm.link/slashdot > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
