Re: [isabelle] [Hol-info] 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 at 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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.