On Dec 17, 2010, at 9:03 AM, Matthew West wrote:
Dear Chris,
Well let's start by confusing the situation with a few facts.
Annoying little suckers, facts. :-)
Barry's criticisms of the use of a non-well-founded set theory like Aczel's
AFA are on the money.
MW: ISO 15926 does say that a class can be a member of itself for reasons
Chris P has alluded to, but it is not committed to a particular form of
non-well foundedness. Aczel is mentioned in an informative note, and there
is an informative annex that gives a lay explanation of some different sorts
of structures sets might have, including well-founded and non-well founded
sets.
That's a good clarification. Barry's comment and my too-hasty look at ISO 15926 suggested AFA or the like was being included as part of the standard.
He notes that it is a greatly overpowered for the needs of the document;
it entails, among other things, the entire massively infinite
hierarchy of transfinite numbers. (How massive? So massive that there
is no transfinite number big enough to number them.)
MW: I don't know why this should be a problem, since there is no commitment
to record them all.
Sure, but the point is more or less Barry's about overkill. Why provide an ontology with a theory that entails an uncountable infinite of things for which the theory has no use? And why make axioms available that could only muddy the waters by getting mixed in with more useful axioms? And there are obviously concerns about automated reasoning when such a powerful underlying theory is part of the ontology; but for the axioms of the theory (the set of theorems of which is provably undecidable), it might be that the ontology could be expressed in a decidable system like OWL DL.
Moreover, ironically, AFA and its like are in a sense underpowered as well for the given task. Notably, as I understand the document, THING is itself a class that contains, well, everything.
MW: Yes. Every upper ontology has such an class, so ISO15926 is not the only one with this problem.
As I've tried to indicate, I do NOT think it is a problem to include a universal class in an ontology. It is a problem only if one tries to model classes as sets in ZF or a ZF-based non-wf theory like AFA.
The existence of such a class (understood as a non-wf set) is flatly inconsistent with non-wf ZF spinoffs like AFA.
MW: I had missed that. Could you give me a section reference (I have Aczel's book).
I gave a proof of the inconsistency using the ZF axiom of separation in a post earlier this morning. AFA and its like are based upon ZF minus the axiom of foundation (as Aczel notes in the introduction to his book) and foundation is inessential to the inconsistency.
Bottom line (as John Sowa likes to say): The underlying class theory of the document needs to be thrown out and rethought completely.
MW: What would you suggest? Not much point kicking up a storm unless you have a better alternative.
Well, that is hardly true. If the bridge is out and I see your train speeding toward it, I'll give your cell a buzz to warn you to get the hell off that train even if I have no suggestions about how you might subsequently reach your intended destination. (And it would hardly be charitable to characterize my solicitous intervention as "kicking up a storm".) Be that as it may, my hunch is that simply using Common Logic as your logical foundation will give you the expressive power to do 90% of what you need and that the rest can probably be achieved with some very simple class existence axioms. Off the top of my head, I might suggest a look at the class theory in SUMO, which explicitly allows for self-membership:
(documentation Class EnglishLanguage "classes differ from sets in three important respects. First, classes are not assumed to be extensional. That is, distinct classes might well have exactly the same instances. Second, classes typically have an associated `condition' that determines the instances of the class. So, for example, the condition `human' determines the class of humans. Note that some classes might satisfy their own condition (e.g., the class ofabstract things is abstract) and hence be instances of themselves. Third, the instances of a class may occur only once within the class, i.e. a class cannot contain duplicate instances.")
Chris Menzel
ps: I am compelled to note that that third respect in which the SUMO documentation for Class says that sets differ from classes is completely confused. Neither sets nor classes can have "duplicate instances". What the SUMO authors probably have in mind here are "bags", which are in reality simply sets whose members have been "tagged" with a positive integer indicating how many times they "occur" in the bag. More exactly, define a bag B to be a pair <B,f> where f maps the set B into {1,2,3,...}. Then, for s ∈ B, whenever f(s) > 1 it can be said that s has "duplicates" in B.
|
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (01)
|