Roger,
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).
>
> In the context of the revised new_specification how do we
> stand in relation to conservative introduction of type
> constructors?
Good point.
> Is it true that in this case the restriction on type
> variables (introduced at the same time as the one in
> new_definition) is without loss of generality of conservative
> extension?
I don't see that. If want to say that a new type can be equipped with the
structure of a free algebra over some signature, then you can't do it with
new_type_definition: you have to use new_type_definition to give a more
concrete description of the free algebra and then derive the abstract property.
I guess I don't mind that so much, since apart from the reasoning done to
define the constructors of the free algebra, thereafter you use the definitions
of the constructors and not the type definition, and my proposal lets you
characterize the constructors abstractly. So I suspect a more abstract version
of new_type_definition could be proposed, but I don't feel strongly motivated
to do so.
Aside: apologies for not noting more explicitly that your original reason for
wanting new_specification was to embrace loose definitions as well as implicit
definitions with a unique witness.
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
