Re: [isabelle] [Hol-info] 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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.