On Saturday 28 Apr 2012 13:14, Rob Arthan wrote: > On 28 Apr 2012, at 09:53, Roger Bishop Jones wrote: > > Is the revised new_specification "complete"? > > i.e. are there any conservative extensions which cannot > > be achieved by it? > > (an argument for this would strengthen the case) > > I would be rather surprised if there were any nice > characterization of what I propose as complete in any > sense. I see new_specification as very much a > work-around for not having quantification over type > variables. There are universal mapping properties that I > don't know how to express without quantification over > type variables. Free groups I can do: to use my proposal > to describe the concept of being a free group, what you > want to say is that G is a free group on a set X iff X > is a subset of the carrier set of G and every function > from X to the carrier set of a group H extends uniquely > to a homomorphism from G to H. You could define this > given my proposal by proving the theorem that if this > property holds for every group H whose carrier set is a > subset of (alpha x 2) LIST where alpha is the type of > the elements G, then it holds for arbitrary H (because > the subgroup generated by a set of cardinality |X| has > cardinality at most |(alpha x 2)LIST|. However, I don't > see how you do any analogue of this for the concept of > being a free complete Boolean algebra, since a > countably-generated complete Boolean algebra can have > arbitrarily large cardinality (P.T. Johnstone, Stone > Spaces, Proposition 4.10).
I think the question I was asking was rather simpler than the one you are trying to answer here. It looks to me like you are asking what can be achieved by conservative extension in HOL and noting, for example that some things that might be said with quantification over types probably can't be said in HOL. 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"? (reflection on the type definition problem now tells me that this should be qualified to exclude the use of new type constructors, i.e. if P is conservative but mentions new type constructors, then you can't get it with new new spec. but otherwise you can) On the matter of new type constructors a similarly "conservative" interpretation of the notion of "completeness" was intended, though it is less clear to me how that can be made precise, and it seems to me that the fact that type constructors can only be introduced one at a time suggests that this mechanism is not so general for types as "new_specification" is (may be?) for constants. The question then arises, by way of approaching the limits of what can be done by conservative extension, whether there might be some more general mechanism which, like the free- set paragraph in Z, might allow both constants and types to be introduced at once? I suspect that might, even if possible, prove complicated. If one does characterise "new_specification" as generalising from definition to conservative extension, it is nevertheless of interest to know how close the fit is. 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
