Re: [isabelle] conservativity of HOL constant and type definitions



Andrei,

> On 24 Oct 2016, at 19:16, Andrei Popescu <A.Popescu at mdx.ac.uk> wrote:
> 
> Since the conservativity topic has been touched upon, I would like to summarize the situation in HOL as I understand it now, after our discussion.   
> (Myself, I am mainly interested in Isabelle/HOL, but this is an important related problem.)   
> Please, correct me if and where I am wrong.
> 
> (1) The constant definition mechanisms (including the more general ones) are known to be:
> (1.1) model-theoretic conservative w.r.t. standard (Pitts) models
> (1.2) model-theoretic conservative w.r.t. Henkin models 
> (1.3) proof-theoretic conservative       
> 
> (2) The type definition mechanism is known to be:    
> (2.1) model-theoretic conservative w.r.t. standard models

I agree with all of the above.

> (2.2) *not* model-theoretic conservative w.r.t. Henkin models (by an easy counterexample -- a Henkin model that does not have the right infrastructure to support a given typedef)
> 
I don't see how to construct a counterexample. Could you give some more details, please.

> Concerning proof-theoretic conservativity of type definitions: there does not exist any proof of this -- or does it? It certainly doesn't follow from (2.1). 

I am pretty sure nothing has been published and, if you are right about (2.2),
then I don't think type definitions can be proof-theoretically conservative.

I have had thoughts about how one might prove that type definitions
are conservative by using relativisation tricks like the ones that are
used to prove that Heyting arithmetic over finite types is conservative
over first-order Heyting arithmetic. I think this problem may well be
sensitive to the choice of non-logical axioms: e.g., it is possible that
type definitions aren't conservative over an intuitionistic fragment of
HOL but are conservative over HOL with AC.

Regards,

Rob.






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