Re: [Hol-info] conservativity of HOL constant and type definitions

[Andrei Popescu]

Hi Ramana,


Thanks for the confirmation (and for the pointer). Yes, the base theories in 
your formalized  result do qualify as arbitrary in my terminology. :-) I assume 
"arbitrary theories" include the usual signature and axioms of polymorphic 
classical higher order logic with equality, Infinity and Choice. Your result is 
more general.


Andrei



From: Ramana Kumar 
Sent: 25 October 2016 08:24
To: Andrei Popescu
Cc: Rob Arthan; Ondřej Kunčar; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; 
cl-isabelle-us...@lists.cam.ac.uk; Roger Bishop Jones; Prof. Peter B. Andrews; 
HOL-info list
Subject: [SPAM: 10.600] Re: [Hol-info] conservativity of HOL constant and type 
definitions

Just to answer the question-mark in (2.1), I mechanised a proof that 
new_type_definition is model-theoretically conservative for standard models and 
arbitrary base theories. To be clear, the proof assumes the base theory 
contains "fun", "bool", and "=", and that it has a model that interprets these 
types/constants in the standard way. I presume this counts as "arbitrary", but 
maybe it doesn't :) (The proof is at 
https://github.com/CakeML/cakeml/blob/master/candle/standard/semantics/holExtensionScript.sml#L366.)

On 25 October 2016 at 09:06, Andrei Popescu 
> wrote:

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 >
Sent: 24 October 2016 21:37
To: Ondřej Kunčar
Cc: Andrei Popescu; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; 
cl-isabelle-us...@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 
> > 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, 

Re: [Hol-info] conservativity of HOL constant and type definitions

[Ramana Kumar]

Just to answer the question-mark in (2.1), I mechanised a proof that
new_type_definition is model-theoretically conservative for standard models
and arbitrary base theories. To be clear, the proof assumes the base theory
contains "fun", "bool", and "=", and that it has a model that interprets
these types/constants in the standard way. I presume this counts as
"arbitrary", but maybe it doesn't :) (The proof is at
https://github.com/CakeML/cakeml/blob/master/candle/standard/semantics/
holExtensionScript.sml#L366.)

On 25 October 2016 at 09:06, Andrei Popescu  wrote:

> 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 
> *Sent:* 24 October 2016 21:37
> *To:* Ondřej Kunčar
> *Cc:* Andrei Popescu; Prof. Andrew M. Pitts; Prof. Thomas F. Melham;
> cl-isabelle-us...@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  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!
>