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 <r...@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-us...@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 <kun...@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.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
