Chris, On a technical note, I am interested in this comment by you: CM: (The central trick here is that, in the semantics of Common Logic, classes *have* extensions but are not *identified* with their extensions in; this makes it easy to allow a class to be in its own extension without any need for non-well-founded set theory. Pat used the same idea when he developed the semantics of RDF.)
I was not aware of this. Are classes intensional objects (I guess, like types)? Could you point me to where in CL this is discussed?
Thanks, Leo From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of Christopher Menzel
Sent: Friday, December 17, 2010 11:58 AM
To: [ontolog-forum]
Subject: Re: [ontolog-forum] [ontology-summit] FW: [ontolog-invitation] Invitation to a brainstorming call for the 2011 Ontology Summit On Dec 17, 2010, at 3:49 AM, Chris Partridge wrote: 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 can see that my initial remark "Barry's criticisms of the use of a non-well-founded set theory like Aczel's AFA are on the money" is a bit ambiguous in that regard.
I realise I should have also included this extract from the RDF Semantics, I probably should have mentioned it myself.
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. No, that is not at all the issue. I agree that It can be a perfectly sensible requirement in an ontology to have a universal class. But ZF-BASED non-well-founded spinoffs like AFA of the sort that Barwise and Moss discuss do NOT provide a way of satisfying that requirement. More exactly: You cannot have a universal class if (a) the basis for your class theory is a ZF-based theory like AFA and (b) you identify classes with the sets of the theory. For such theories are inconsistent with the existence of a universal class. Here's a simple proof. Suppose there is a universal class U, i.e., an AFA-set U such that for all x, x ∈ U. The axiom of separation (a ZF-axiom that AFA inherits) says that, for any set A and any description φ, there is a set containing all the members of A satisfying φ(x); a bit more formally, separation says that, for set A and description φ, the set {x ∈ A : φ(x)} exists. So let R be the set {x ∈ U : x ∉ x}. Since everything is an element of U, R is identical to {x : x ∉ x}, and that is the Russell set, the existence of which immediately entails the contradiction that R ∈ R if and only if R ∉ R, by a familiar argument. 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.
As just indicated, non-wf set theories of the sort that Barwise and Moss study do not provide a solution to the problem of having a universal class. Just because a universal class would be non-well-founded does not mean that the existence of such a class is compatible with non-well-founded set theory.
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). Common Logic itself does not include ZF (though ZF or the like is implicitly used for its metatheory). It is simply the case that (as Barry also notes in his paper) Common Logic permits self-exemplifying classes; more exactly, if C is a class, the _expression_ C(C) (which you could, by convention, alternatively write as C ∈ C) is syntactically well-formed and means (as it should) that C is a member of its own extension. (The central trick here is that, in the semantics of Common Logic, classes *have* extensions but are not *identified* with their extensions in; this makes it easy to allow a class to be in its own extension without any need for non-well-founded set theory. Pat used the same idea when he developed the semantics of RDF.)
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? Yes, although there other (in my view, considerably more serious) difficulties that would arise such theories as well (e.g., Quine's NF). Chris Menzel
From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of Christopher Menzel
Sent: 17 December 2010 04:00
To: [ontolog-forum]
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. For example,
http://www.amazon.co.uk/gp/product/1575860082/ref=wms_ohs_product
Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena - Jon
Barwise (Author), Lawrence Moss (Author)
Product Description
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
your foundation.
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.
Chris
-----Original Message----- On Dec 16, 2010, at 2:24 PM, Matthew West wrote:
-1 for 15926, with arguments:
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/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontology-summit/
Unsubscribe: mailto:ontology-summit-leave@xxxxxxxxxxxxxxxx
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/
|
_________________________________________________________________
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)
|