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



On 10/24/2016 10:37 PM, Rob Arthan wrote:
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.

I think Andrei wanted to point out that a Henkin model doesn't have to contain all the subsets and this would prevent us to extend the model to a model of the theory in which typedef was done for one of the missing subsets. But I guess you are saying that the model should include at least those subsets that are definable by a formula.

Or have I misunderstood something?

Ondrej




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