Email Gateway (Aug 22 2022 at 14:21): Email Gateway (Aug 22 2022 at 14:21):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Since the conservativity topic has been touched upon, I would like to summarize the situation in HOL as I understand it now, after our discussion.
(Myself, I am mainly interested in Isabelle/HOL, but this is an important related problem.)
Please, correct me if and where I am wrong.
(1) The constant definition mechanisms (including the more general ones) are known to be:
(1.1) model-theoretic conservative w.r.t. standard (Pitts) models
(1.2) model-theoretic conservative w.r.t. Henkin models
(1.3) proof-theoretic conservative
(2) The type definition mechanism is known to be:
(2.1) model-theoretic conservative w.r.t. standard models
(2.2) not model-theoretic conservative w.r.t. Henkin models (by an easy counterexample -- a Henkin model that does not have the right infrastructure to support a given typedef)
Concerning proof-theoretic conservativity of type definitions: there does not exist any proof of this -- or does it? It certainly doesn't follow from (2.1).
Best,
Andrei
Email Gateway (Aug 22 2022 at 14:22):From: Rob Arthan <rda@lemma-one.com>
Andrei,
On 24 Oct 2016, at 19:16, Andrei Popescu <A.Popescu@mdx.ac.uk> wrote:
Since the conservativity topic has been touched upon, I would like to summarize the situation in HOL as I understand it now, after our discussion.
(Myself, I am mainly interested in Isabelle/HOL, but this is an important related problem.)
Please, correct me if and where I am wrong.(1) The constant definition mechanisms (including the more general ones) are known to be:
(1.1) model-theoretic conservative w.r.t. standard (Pitts) models
(1.2) model-theoretic conservative w.r.t. Henkin models
(1.3) proof-theoretic conservative(2) The type definition mechanism is known to be:
(2.1) model-theoretic conservative w.r.t. standard models
I agree with all of the above.
(2.2) not model-theoretic conservative w.r.t. Henkin models (by an easy counterexample -- a Henkin model that does not have the right infrastructure to support a given typedef)
I don't see how to construct a counterexample. Could you give some more details, please.
Concerning proof-theoretic conservativity of type definitions: there does not exist any proof of this -- or does it? It certainly doesn't follow from (2.1).
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 have had thoughts about how one might prove that type definitions
are conservative by using relativisation tricks like the ones that are
used to prove that Heyting arithmetic over finite types is conservative
over first-order Heyting arithmetic. I think this problem may well be
sensitive to the choice of non-logical axioms: e.g., it is possible that
type definitions aren't conservative over an intuitionistic fragment of
HOL but are conservative over HOL with AC.
Regards,
Rob.
Email Gateway (Aug 22 2022 at 14:22):From: Ondřej Kunčar <kuncar@in.tum.de>
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.
Ondrej
Email Gateway (Aug 22 2022 at 14:22):From: Ondřej Kunčar <kuncar@in.tum.de>
should have been: ... you cannot use the approach as you did
for constants.
Email Gateway (Aug 22 2022 at 14:22):From: Rob Arthan <rda@lemma-one.com>
Ondrej,
On 24 Oct 2016, at 20:32, Ondřej Kunčar <kuncar@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.
Email Gateway (Aug 22 2022 at 14:22):From: Ondřej Kunčar <kuncar@in.tum.de>
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
Email Gateway (Aug 22 2022 at 14:22):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
The counterexample I had in mind is due to Makarius Wenzel (https://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf, page 8): The theory T containing the single HOL formula "no type has cardinal 3" has a Henkin model M; yet, M has no expansion to the theory T extended with the definition of the type {1,2,3}. But actually this extension is not proof-theoretically conservative either (as it even breaks consistency) ...
In fact, now I see that I have not clearly spelled out all the assumptions of the statements in my summary. So let me try again, also factoring in the base (i.e., to-be-extended) theory:
(1) The constant definition mechanisms (including the more general ones) are known to be:
(1.1) model-theoretic conservative w.r.t. standard (Pitts) models and arbitrary base theories
(1.2) model-theoretic conservative w.r.t. Henkin models and arbitrary base theories
(1.3) proof-theoretic conservative and arbitrary base theories
(2) The type definition mechanism is known to be:
(2.1) model-theoretic conservative w.r.t. standard models and arbitrary(?) base theories
and known not to be:
(2.2) model-theoretic conservative w.r.t. Henkin models and arbitrary base theories
(2.3) proof-theoretic conservative w.r.t. Henkin models and arbitrary base theories
On the other hand, it is of course legitimate to lower the expectation for typedefs, so we could ask what happens with (2.2) and (2.3) if we restrict to base theories that are themselves definitional. Here, the above counterexample does not work. And yes, Rob, without being able to follow your Heyting arithmetic analogy, I do see the similarity between a possible semantic proof of definitional-base-(2.2) and a possible syntactic proof of definitional-base-(2.3) (both revolving around the notion of relativization to sets).
But I am surprised that a lot of attention has been given to the conservativity of constant definitions/specifications, but not to that of the old and venerable typedef.
Best,
Andrei
From: Rob Arthan <rda@lemma-one.com>
Sent: 24 October 2016 21:37
To: Ondřej Kunčar
Cc: Andrei Popescu; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-users@lists.cam.ac.uk; Roger Bishop Jones; Prof. Peter B. Andrews; HOL-info list
Subject: Re: conservativity of HOL constant and type definitions
Ondrej,
On 24 Oct 2016, at 20:32, Ondřej Kunčar <kuncar@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.
Last updated: Nov 21 2024 at 12:39 UTC