Andrei,
Here is an "interesting sufficient condition" for model-theoretc
conservativity to entail proof-theoretic conservativity, particularly
relevant to the present discussion:
If in T there is a theorem asserting that an extension is
model-theoretically conservative, in the form required by the old
version of "new_specification" i.e. asserting the existence (implicitly
in every model) of values satisfying some predicate, then the extension
obtained by asserting that property of some group of new constants will
be proof-theoretically conserative.
We know that this is the case because the theorem enables us to
introduce a conservative extension using a simple definition and the
choice function which includes the intended extension (and some other
stuff, but, conservative assuming that simple definition is conservative).
Probably this rationale extends also to the more recent version of
"new_specification", maybe even to the yet stronger version not
implemented which would allow simultaneous extension with constants and
type constructors.
Roger Jones
On 23/10/2016 14:31, Andrei Popescu 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.
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
