On Wed, Jul 9, 2008 at 11:29 AM, Ralf Hemmecke wrote:
>> 1) Domain is the domain whose values are domains.
>>
>> Is this ok?
>
> This says that Domain contains itself as a value.
>
Yes.
>> 2) A category is some specified subdomain (subset) of Domain?
>
> This doesn't explain what a category is, but only that all categories are
> contained in Domain and thus are called 'domain's.
No. I said that category is some "part of" Domain - not "contained in"
in the way that a set contains elements but rather a like a subset. We
do not know yet at this point in the definition whether such subsets
are also contained in Domain.
> Unfortunately, that "specific subdomain of Domain" could be empty, so I don't
> know
> whether there are categories at all. ;-)
>
Yes, the empty set (empty category) would exist by this definition. In
a sense it is the opposite of the category 'with {}'. No domain
satisfies the empty category, i.e.
x has EmptyCategory
would always return false. Right now I can't think of a reason why we
might need it.
But this does *not* mean that there are not categories at all!
>> I.e. The subset of Domain corresponding to a category is given by the
>> domains which refer to specific categories in their definition.
>
>> 3) A subdomain need not be a proper subset, i.e. it can consist of all
>> of Domain as a whole.
>>
>> In set theory X is an element of the power set power(X).
>
> I think comparing subdomain with subset makes it clear enough for me.
>
In Axiom the domain 'Set R' is the domain whose values are finite
subsets of values from R.
>> 4) Category is the domain of categories, i.e. subdomains of Domain. As
>> such it corresponds to the concept of the power set of Domain.
>
> Don't you mean to an "element of the power set of Domain", i.e. Categoy is a
> subdomain/subset of Domain?
>
No. Category *is* the power set consisting of all such subsets. It's
values are categories (subdomains of Domain).
>> 5) Type is the category in Category corresponding to Domain. In other
>> words Type is Domain in Category.
>
> That sound like "Domain: Type". But we also have "Type: Category" and
> "Category \subdomain Domain". That says that "Type: Domain" is also OK.
>
> That looks all too circluar to me.
>
The definition is ultimately circular. That is why I referred in an
earlier message to the theory of "non-well-founded sets". I don't
think this is a problem.
I am not sure what you mean by "Domain: Type". I said: Type is a value
(constant) contained in Category. (Remember Category is the power set
construction on Domain). When I said "Type is Domain" what I mean is
that Type is the constant value in Category that corresponds to the
set consisting of all of the values of Domain.
>> Just like X in power(X).
>
>>> Somehow I now have the impression that Aldor-Type and OpenAxiom-Type
>>> are different.
>>
>> Yes. According to my definition they are different.
>>
>>> That "Type" is a category in OpenAxiom would have never come to
>>> my mind in Aldor.
>
>> Type in OpenAxiom is like 'with {}' in Aldor. Until Saul Yousseph
>> presented his ideas on implementing mathematical category theory in
>> Aldor perhaps no one thought this category was particularly
>> interesting.
>
> But Saul defines
>
> Domain: Category == with
>
> so that is yet another occurence of "Domain".
I am not sure what you mean by "occurence". But I think the answer is
"no". 'Domain' as defined by Saul in Aldor is a category, so it is
subdomain of Domain in OpenAxiom.
> Would you say that in Aldor
> this Youssef-"Domain" is what "Type" is in panAxiom?
>
Yes.
Regards,
Bill Page.
-------------------------------------------------------------------------
Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
Studies have shown that voting for your favorite open source project,
along with a healthy diet, reduces your potential for chronic lameness
and boredom. Vote Now at http://www.sourceforge.net/community/cca08
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
