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



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.

They could. You can try to argue by "unfolding" the type definitions. 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 use the approach as you did for constants.

Ondrej




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