On Sunday 29 Apr 2012 11:11, Rob Arthan wrote: > > The question I was asking was rather more mundane. > > Given that we know what it means to say that some > > proposition P is conservative over a given theory in > > HOL (in the proof theoretic sense), the question is > > "is there any proposition, P, conservative over some > > HOL theory, which cannot be introduced using the new > > "new_specification" in the context of that theory?" > > Isn't there a fairly obvious proof that the answer is > > "no"? > > I conjecture your fairly obvious proof starts with the > observation that HOL is sound and complete with respect > to its general models (where "general" means not > necessarily standard) and concludes by saying that > something that exists in all general models provably > exists in all general models and hence can be defined > using new_specification. Is that right?
That's not what I had in mind. The "obvious proof" which occurred to me runs like this: If P is conservative over T then any Q provable in T+P but not containing any of the new constants introduced by P must also be provable in T. So the existential claim E obtained by replacing the new constants in P by new variables and then existentially binding them will be a theorem of T (proved in T+P using the constants as witnesses, and hence somehow provable in T). We can therefore get witnesses for E which do not mention the constants by using the choice function on the body of E, and these witnesses can be used in the assumptions of a theorem of the form necessary to introduce P with the new "new_specification". Hence any (closed) P which is conservative over some theory T (and does not contain any new type constructors) can be introduced by the new "new_specification". This is the "completeness" result I was looking for (though not the kind of completeness you might have liked for introducing structures using universal properties). If, therefore, "new_specification" is billed as providing for the introduction of constants by conservative extension, the case for the proposed enhancement is bolstered by the result that it provides an optimal solution, in that the extensions which can be obtained using it are exactly the conservative extensions which only involve new constants, i.e. an extension P (not involving new types) can be obtained through the new feature iff it is conservative. The proof of this is in two parts, the first of which is your conservativeness proof and the other direction is the proof sketched above. And of course, this desirable property is not posessed by the existing "new_specification", because the type variable constraint prevents some conservative extensions from being accepted. Roger Jones ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
