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.


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