On 28 Apr 2012, at 16:17, Roger Bishop Jones wrote:
> 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).
Oops! That should be I.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"?
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?
I had in mind something more intensional. Given a class of algebraic structures
modelled by a polymorphic type alpha THING, there is the standard notion of a
free structure A (of type alpha THING) over a set X (of type alpha SET), One
would like to define this notion as a HOL function FreeThing : alpha THING x
alpha SET -> BOOL such that FreeThing (A, X) holds iff for all B : beta THING
and all functions f : alpha -> beta, there exists a unique THING-morphism g :
alpha -> beta that agrees with f on X. (I am suppressing some details about
substructures and carrier sets here, that would be needed in a real treatment).
But you can't define FreeThing in general with the existing or the proposed
revision to new_specification. For structures with finitary operations like
groups, you can do it but you need to do some proof to show that the property
with beta instantiated to a fixed function of alpha implies the general
property. If you have infinitary operations as in complete Boolean algebras you
are in trouble. Extensionally, Johnstone's proposition I.4.10 tells us that
free complete Boolean algebras don't exist, so we can define
FreeCompleteBooleanAlgebra using new_definition thus:
FreeCompleteBooleanAlgebra (A, X) = false
Methodologically, this isn't satisfactory, but I think without quantification
over type variables you just have to live with it.
Aside: has anyone formalised a proof that free complete Boolean algebras don't
exist?
> (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.
Yes, one could certainly consider a mechanism for defining mutually dependent
new types - in fact I am slightly surprised that the implementors of recursive
types packages haven't proposed this. However, I expect that everything you
could in principle do with a mechanism for defining mutually dependent new
types could be achieved by forming a subtype of a disjoint union and then
forming subtypes of that. (Is that how the various recursive types packages do
it?)
>
> 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.
>
In my experience, it is quite common for the defining property for a type just
to assert the existence of constructors and destructors with appropriate
properties. This is used once to define the constructors and destructors and
then never used again. In such a case it would save a little bit of clutter to
have a combined mechanism. The choice would seem to be between one more
complicated mechanism and a little bit less clutter or two simpler mechanisms a
little bit of extra clutter. I think i am in favour of the latter.
Regards,
Rob.
------------------------------------------------------------------------------
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
