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 ------------------------------------------------------------------------------ The Command Line: Reinvented for Modern Developers Did the resurgence of CLI tooling catch you by surprise? Reconnect with the command line and become more productive. Learn the new .NET and ASP.NET CLI. Get your free copy! http://sdm.link/telerik _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
