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



Ondrej,

> On 24 Oct 2016, at 20:32, OndÅej KunÄar <kuncar at in.tum.de> wrote:
> 
> On 10/24/2016 09:16 PM, Rob Arthan wrote:
>> 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 made that sound too strong: I was just making a conjecture: for "think" read "feel".

> They could. You can try to argue by "unfolding" the type definitions.

"Unfolding" of types is exactly what I had in mind when I mentioned
the methods used in connect with Heyting arithmetic. 

> Again, the model-theoretic conservativity is stronger than the proof-theoretic in general. And here you don't have an existential quantifier for type constructors so you [can't] use the approach as you did for constants.

Yes, but if the unfolding approach works, you would have reduced the
essential properties of the type definition to a statement about the existence
of a certain subset of the representation type bearing a relationship with some
siubsets of the parameter types and you would then be able to deduce
model-theoretic conservativeness. That's why I felt, that if Andrei is right that
the type definition principle is not model-theoretically conservative w.r.t.
Henkin models (his point (2.2)), then it won't be proof-theoretically conservative
either, because the unfolding argument must break down somewhere.
It would be very useful to see an example of a type definition that is not
conservative w.r.t. Henkin models.

Regards,

Rob.







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