Email Gateway (Aug 22 2022 at 14:20): Email Gateway (Aug 22 2022 at 14:20):From: Scott Owens <S.A.Owens@kent.ac.uk>
I don’t want to put words in Rob’s mouth, as he’s far more knowledgable in this area than I am.
As far as I know, there is no mechanised conservativity proof for HOL’s recent generalised constant specification mechanism. (Here I’m in agreement that “conservativity” without any other modification should refer to the proof theoretic notion, and that’s what I mean here.) Rob certainly has a pencil-and-paper proof. Ramana, Rob, Magnus, and I (although mostly Ramana) proved the soundness of a HOL Light-style logical system, including the generalised constant specification mechanism that Rob refers to (and also designed) and type definition mechanism, with respect to a standard model of higher-order logic. I worked on a mechanised conservativity proof for the definition mechanism for a bit two years ago but got distracted and haven’t returned to it. I think it would be a suitable student project, but I’m not convinced that it’s really that interesting — I wouldn’t be bothered by a sound and consistent definition principle that allowed one to prove more things.
Scott
Email Gateway (Aug 22 2022 at 14:21):From: Rob Arthan <rda@lemma-one.com>
Scott,
Apologies if I claimed you had formalised more than you actually did.
Regards,
Rob.
Email Gateway (Aug 22 2022 at 14:21):From: Rob Arthan <rda@lemma-one.com>
Ondrej,
On 22 Oct 2016, at 20:07, Ondřej Kunčar <kuncar@in.tum.de> wrote:
Hi Rob,
you are right that we mention only the plain definitions in HOL and not
the implicit ones, when we compare the definitional mechanism of HOL and
Isabelle/HOL. (If this what you meant; I assume you didn't mean to say
that the overloading in Isabelle is 25 years out of date).
No. I was just referring to new_specification.
I clearly remember that one of the early versions of our paper contained
the comment that the current HOL provers use the more powerful mechanism
that you mentioned but I guess that it was lost during later editing. We
will include it again into the journal version of the paper.Thanks. I’m glad I raised my comment in time for you to do that.
I wanted to comment on your statement that A. Pitts proved that
definitions in HOL are conservative. Such statements are always a little
bit puzzling to me because when you say conservative (without any
modifier), I always think that you mean the notion that "nothing new can
be proved if you extend your theory (by a definition)". I think a lot of
people (including me) think that this is THE conservativity. There is
also a notion of the model-theoretic conservativity that requires that
every model of the old theory can be expanded to a model of the new
theory. This is a stronger notion and implies the proof conservativity.
It’s the other way round. Soundness implies that proof-theoretic
conservativity implies model-theoretic conservativity. In the absence of
completeness, an x with some property phi(x) might exist in every model,
but you might not be able to prove that. Taking phi(c) as the defining
property of a new constant c would then be conservative model-theoretically
but not proof-theoretically.
As far as I know, A. Pitts considers only a subset of all possible
models (so called standard models) in his proof and he only proves that
these models can be extended from the old to the new theory. But as far
as I know this does not imply the proof conservativity.
Andy Pitts gives a proof of the model-theoretic conservativity of new_specification
with respect to standard models. You are quite right that in the absence of completeness
this is a weaker result than proof-theoretic completeness. I don’t think it’s difficult
to extend the result to general models (Henkin models) and so get proof-theoretic conservativity.
I suspect Andy just didn’t want to introduce a lot of extra technical detail.
I proved proof-theoretic conservativity for the new mechanism gen_new_specification.
As new_specification is derivable using gen_new_specification, this gives you
proof-theoretic conservativity for both. (Thanks to Scott for correcting my statement
about what has been formalised so far in HOL4).
Regards,
Rob.
Email Gateway (Aug 22 2022 at 14:21):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Rob,
It’s the other way round. Soundness implies that proof-theoretic conservativity implies model-theoretic conservativity.
Ondra's statement was the correct one.
Let's spell this out, to make sure we are speaking of the same thing. Say you have a signature Sigma' extending a signature Sigma (by adding some constant and type constructor symbols). Then every Sigma'-model M' produces a Sigma-Model, Forget(M'), by forgetting the interpretation of the symbols in Sigma' minus Sigma. Moreover,
(*) For every closed Sigma-formula phi, we have that M |= phi holds iff Forget(M) |= phi holds.
Let T be a Sigma-theory (i.e., a set of closed Sigma-formulas), and let T' be a Sigma'-theory that includes T.
T' is called:
(A) a model-theoretic conservative extension of T if, for all Sigma-models M of T, there exists a Sigma'-model M' of T' such that Forget(M') = M.
(B) a proof-theoretic conservative extension of T if, for all closed Sigma-formulas phi, T' |- phi implies T |- phi.
Assuming soundness and completeness, we have (A) implies (B). Proof: We can reason about semantic deduction |= instead of syntactic deduction. Assume T'|= phi .To prove T|= phi, let M |= T; by (A), we find M' |= T' such that Forget(M') = M. With T'|= phi, we obtain Forget(M')|= phi. From this and (*), we obtain M' |= phi, as desired.
In general, (B) does not imply (A), and I don't know of interesting sufficient conditions for when it does.
Best,
Andrei
From: Rob Arthan <rda@lemma-one.com>
Sent: 23 October 2016 12:23
To: Ondřej Kunčar
Cc: Ken Kubota; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-users@lists.cam.ac.uk; Roger Bishop Jones; Prof. Peter B. Andrews; Andrei Popescu; HOL-info list
Subject: Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
Ondrej,
On 22 Oct 2016, at 20:07, Ondřej Kunčar <kuncar@in.tum.de> wrote:
Hi Rob,
you are right that we mention only the plain definitions in HOL and not
the implicit ones, when we compare the definitional mechanism of HOL and
Isabelle/HOL. (If this what you meant; I assume you didn't mean to say
that the overloading in Isabelle is 25 years out of date).
No. I was just referring to new_specification.
I clearly remember that one of the early versions of our paper contained
the comment that the current HOL provers use the more powerful mechanism
that you mentioned but I guess that it was lost during later editing. We
will include it again into the journal version of the paper.Thanks. I’m glad I raised my comment in time for you to do that.
I wanted to comment on your statement that A. Pitts proved that
definitions in HOL are conservative. Such statements are always a little
bit puzzling to me because when you say conservative (without any
modifier), I always think that you mean the notion that "nothing new can
be proved if you extend your theory (by a definition)". I think a lot of
people (including me) think that this is THE conservativity. There is
also a notion of the model-theoretic conservativity that requires that
every model of the old theory can be expanded to a model of the new
theory. This is a stronger notion and implies the proof conservativity.
It’s the other way round. Soundness implies that proof-theoretic
conservativity implies model-theoretic conservativity. In the absence of
completeness, an x with some property phi(x) might exist in every model,
but you might not be able to prove that. Taking phi(c) as the defining
property of a new constant c would then be conservative model-theoretically
but not proof-theoretically.
As far as I know, A. Pitts considers only a subset of all possible
models (so called standard models) in his proof and he only proves that
these models can be extended from the old to the new theory. But as far
as I know this does not imply the proof conservativity.
Andy Pitts gives a proof of the model-theoretic conservativity of new_specification
with respect to standard models. You are quite right that in the absence of completeness
this is a weaker result than proof-theoretic completeness. I don’t think it’s difficult
to extend the result to general models (Henkin models) and so get proof-theoretic conservativity.
I suspect Andy just didn’t want to introduce a lot of extra technical detail.
I proved proof-theoretic conservativity for the new mechanism gen_new_specification.
As new_specification is derivable using gen_new_specification, this gives you
proof-theoretic conservativity for both. (Thanks to Scott for correcting my statement
about what has been formalised so far in HOL4).
Regards,
Rob.
Email Gateway (Aug 22 2022 at 14:21):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Rob,
As discussed off-list with you and Ondrej, the case covered by new_specification or gen_new_specification is one where (B) implies (A).
Indeed. Many thanks (to you and Roger) for the clarifications.
Of course, none of the above works for an extension that introduces new types.
Your paper is a very nice contribution to the problem of defining new types.
Thanks. Also, thanks for bringing up new_specification and gen_new_specification. After having a closer look at them, I see that the definitional dependency analysis we introduce in the paper can be easily extended to cope with these mechanisms -- which means that they don't raise additional difficulties in the delicate balance between constant overloading and typedef, and therefore are in principle suitable for Isabelle/HOL. We'll add a discussion of this in the journal version (and point you to it when it's available).
Best,
Andrei
From: Rob Arthan <rda@lemma-one.com>
Sent: 23 October 2016 22:56
To: Andrei Popescu
Cc: Ondřej Kunčar; 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: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
Andrei,
On 23 Oct 2016, at 14:31, Andrei Popescu <A.Popescu@mdx.ac.uk> wrote:
Hi Rob,
It's the other way round. Soundness implies that proof-theoretic conservativity implies model-theoretic conservativity.
Ondra's statement was the correct one.
Let's spell this out, to make sure we are speaking of the same thing. Say you have a signature Sigma' extending a signature Sigma (by adding some constant and type constructor symbols). Then every Sigma'-model M' produces a Sigma-Model, Forget(M'), by forgetting the interpretation of the symbols in Sigma' minus Sigma. Moreover,
(*) For every closed Sigma-formula phi, we have that M |= phi holds iff Forget(M) |= phi holds.
Let T be a Sigma-theory (i.e., a set of closed Sigma-formulas), and let T' be a Sigma'-theory that includes T.
T' is called:(A) a model-theoretic conservative extension of T if, for all Sigma-models M of T, there exists a Sigma'-model M' of T' such that Forget(M') = M.
(B) a proof-theoretic conservative extension of T if, for all closed Sigma-formulas phi, T' |- phi implies T |- phi.
Assuming soundness and completeness, we have (A) implies (B). Proof: We can reason about semantic deduction |= instead of syntactic deduction. Assume T'|= phi .To prove T|= phi, let M |= T; by (A), we find M' |= T' such that Forget(M') = M. With T'|= phi, we obtain Forget(M')|= phi. From this and (*), we obtain M' |= phi, as desired.
In general, (B) does not imply (A), and I don't know of interesting sufficient conditions for when it does.
As discussed off-list with you and Ondrej, the case covered by
new_specification or gen_new_specification is one where (B) implies (A).
The interesting sufficient conditions that apply are; (1) T' is a finitely axiomatizable
expansion of T introducing finitely many new constants and no new types
and (2) the logical language admits an existential quantifier
with the usual proof rules and semantics. For then if T' satisfies (B), let
phi(x_1, ... x_n) denote the result of taking the conjunction of the formulas
that axiomatize T' and replacing the new constants c_1, ..., c_n
by variables x_1, ..., x_n. Then T' proves psi ::= exists x_1, ... , x_n. phi(x_1, ..., x_n).
By (B), T proves psi, but then, by soundness, psi holds in every model of T, which implies (A).
Of course, none of the above works for an extension that introduces new types.
Your paper is a very nice contribution to the problem of defining new types.
Regards,
Rob.
Last updated: Apr 26 2024 at 08:19 UTC