Ondrej, > On 22 Oct 2016, 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).
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. ------------------------------------------------------------------------------ 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
