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. ------------------------------------------------------------------------------ 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
