Ondrej, > On 24 Oct 2016, at 20:32, Ondřej Kunčar <kun...@in.tum.de> wrote: > > 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. I made that sound too strong: I was just making a conjecture: for "think" read "feel".
> They could. You can try to argue by "unfolding" the type definitions. "Unfolding" of types is exactly what I had in mind when I mentioned the methods used in connect with Heyting arithmetic. > 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. Regards, Rob. ------------------------------------------------------------------------------ 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
