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 <r...@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-us...@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.pope...@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.
------------------------------------------------------------------------------
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!
http://sdm.link/telerik
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
