OK, I see we may have been talking at cross purposes.
My concern was your criticism could be read as a comment on the requirement rather than the particular axiomatisation. I realise (now) that this is not what you intended. But if I made this mistake, it is possible (likely) others did too.
I realise I should have also included this extract from the RDF Semantics,
For example, it is quite OK for (the extension of) a 'universal' class to contain the class itself as a member, a convention that is often adopted at the top of a classification hierarchy. (If an extension contained itself then the axiom would be violated, but that case never arises.) The technique is described more fully in [Hayes&Menzel].
OK, so the issue is not that it is a sensible requirement to have a universal class as Barwise and Moss suggest. I hope I have not misread that J.
But you are, it seems to me, taking issue with Barwise and Moss’s suggestion for a solution – non-well founded set theory – at least in this case.
My recollections (from some time ago) is that a lot of the motivational examples could easily appear in ISO 15926 ontologies. However, you are much closer to the topic, so maybe my recollections are false.
I am guessing, but from Pat’s comment above about your joint paper, it would seem you agree that this is a common requirement (and you have found a way of finessing this within standard ZF).
I am also (maybe mistakenly again) reading between the lines that the consistency issue arises with “ZF-based non-wf set theories like AFA” and so non-ZF based type theories would avoid this issue. Would you want to use your point #1 (overkill) arguments against these?
From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of Christopher Menzel
Sent: 17 December 2010 04:00
Cc: Ontology Summit 2011 discussion
Subject: Re: [ontolog-forum] [ontology-summit] FW: [ontolog-invitation] Invitation to a brainstorming call for the 2011 Ontology Summit
[Redirecting from the Ontology Summit list to Ontolog forum — followups should be directed solely to the latter list.]
On Dec 16, 2010, at 4:37 PM, Chris Partridge wrote:
Not every logician agrees with Chris (which I am sure is no surprise to anyone - including Chris).
Chris: That is assuredly true, but what I fear you have grossly misunderstood my previous post if you think that the citations you listed show some disagreement between me and the likes of Barwise and Moss. Nothing I said was in any way a criticism of non-wf set theory (as the quotes you included in your post would suggest). Indeed, as a postdoc, I had the pleasure of attending a seminar (along with Barwise) in which we went through a draft of what was to become Aczel's well-known text on the subject. (Larry Moss was in fact a fellow postdoc but, somewhat curiously in hindsight, I don't recall him attending the seminar.) I have been a big fan of the subject ever since. Barwise and Moss's terrific book Vicious Circles, in particular, contains both brilliant exposition and a series of impressive applications of the theory to very difficult topics in philosophy, semantics, and computation — topics whose complexity and subtlety require extraordinarily powerful mathematical tools. My post had nothing to do with such work; it had only to do with the adoption of non-wf set theory by the authors of ISO 15926.
Point #1: While the full power non-wf set theories like AFA that are based on ZF (minus the axiom of foundation, of course) is necessary for the sorts of complex applications taken up in Vicious Circles and the like, such set theories are (as Barry had already pointed out) massive overkill for ISO 15926. (In particular, I assume that the ontology has no need for the entire class of transfinite ordinals, power sets of uncountable sets, and so on.)
Point #2: On the assumption that it is a "theorem" of ISO 15926 that (a) THING is a class and (b) everything is a member of THING, ISO 15926 is flatly inconsistent with ZF-based non-wf set theories like AFA, in which it is a theorem that there is no such class as THING.
Unless the authors of ISO 15926 don't care that their ontology is provably inconsistent, they need a very different class theory.
Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena - Jon
Barwise (Author), Lawrence Moss (Author)
Circular analyses of philosophical, linguistic, or computational phenomena
have been attacked on the assumption that they conflict with mathematical
rigour. Barwise and Moss have undertaken to prove this assumption false.
This volume is concerned with extending the modelling capabilities of set
theory to provide a uniform treatment of circular phenomena.
Jon Barwise (http://en.wikipedia.org/wiki/Jon_Barwise ) argues that the
circularity found in non-well-foundedness is common in the real world - i.e.
it is a common requirement. As such it would make sense to include it on
While personally not finding all his examples persuasive, I think the
general point that it is a requirement is well made.
Another interesting recent (technical) book on a similar the same topic is http://www.amazon.co.uk/gp/product/0199276439/ref=wms_ohs_product - Absolute Generality - Agustín Rayo (Editor), Gabriel Uzquiano (Editor). I believe the introduction can be found somewhere on the net.
On Dec 16, 2010, at 2:24 PM, Matthew West wrote:
-1 for 15926, with arguments:
Which are answered in: [THIS LINK]
Barry's criticisms of the use of a non-well-founded set theory like Aczel's
AFA are on the money. 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.) 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. The existence of such a class (understood as a
non-wf set) is flatly inconsistent with non-wf ZF spinoffs like AFA.
Bottom line (as John Sowa likes to say): The underlying class theory of
the document needs to be thrown out and rethought completely.
Msg Archives: http://ontolog.cim3.net/forum/ontology-summit/
Community Files: http://ontolog.cim3.net/file/work/OntologySummit2011/
Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OntologySummit2011
Community Portal: http://ontolog.cim3.net/wiki/ (01)