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
This archive was generated by a fusion of
Pipermail (Mailman edition) and