- From: Pat Hayes <phayes@ai.uwf.edu>
- Date: Fri, 5 Apr 2002 15:53:38 -0600
- To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>
- Cc: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, <dieter@cs.vu.nl>, <www-webont-wg@w3.org>
>Basically agreeing with Pat, see on, Hmm, Im not sure if we really do agree. See below. > >Peter: >> >I claim that this precisely captures the intuitive meaning of my example. >> >Given an OWL KB, I need to be able to determine if an object in that KB >> >satisfies a restriction that is not necessarily mentioned in the KB. >> >I would be prepared to do this somewhat indirectly, as in >> > >> > <John, child, Joe>, <Joe, rdf:type, Person> >> > |= <John, rdf:type, :_2>, <:2, owl:sameAs?, :_1>, >> > <:_1, owl:onProperty, child>, <:_1, owl:hasClass, Person> >> > >> >However, I view any approach that does not come up with some way of doing >> >the above as fundamentally broken. > >Pat: >> Yes, this is a very intense disagreement between us. I view your way >> of thinking here as itself totally broken. It insists on reducing all >> of logic to inferences in set theory, a perspective I have never even >> seen expressed before in any forum, logical or otherwise. I have >> always thought of DLs as a restricted form of logic, but you seem to >> have a completely different perspective, in which DL's are a branch >> of set theory,and even elementary logical reasoning has been >> eliminated in favor of set-theoretic constructions. >> >> Can you give us any reason at all why we should take this idea seriously? >> >> Pat >> > > > >Set theory is believed to be a solved problem, but the best solutions (e.g. >ZF) are complicated. I think in the sort of approaches that both Pat and I >have been arguing for, the set theory is solved outside OWL. At some level >the awkward examples occur because DAML+OIL (and OWL) embed a relatively >naive way of talking about sets. If we try and construct a set theory in >this naive way then we hit trouble. First, set theory has come quite a long way since Zermelo, and it seems much clearer now that we in fact do not need to be so worried about the axiom of foundation as those guys in the 1940s were. But that's a minor point in this debate; the real issue, for me, is why we are talking about set theory at all. I thought that description logic was a LOGIC, not a set theory: in fact, that it was a restricted subset of first-order logic, and that the restrictions were there essentially for computational reasons, in order to guarantee that inference processes (query answering processes, in particular) would terminate in a reasonable time (or at least in some time, anyway) and always give full answers to all queries, etc.. From this perspective, the syntactic constructions of OIL and DAML and all the other languages in this style, are only packaged forms of logical expressions: a property is a binary relation, a class is a predicate, and so on. That seems to be the intuitive picture underlying RDF(S), for sure. But I'm slowly coming to see that for Peter, at least, DLs are a much more radical notion than just a restricted logic. They are a fundamentally different way of viewing the world, one where the way to assert or query what I would call a sentence or a proposition is to refer to a *set-theoretic construction* and assert that, or ask whether, it *exists*. There are no actual propositions or sentences left, other than those about set theory. So questions about my grandmother's canaries are transformed into questions about the existence of a set-theoretical construct, a question that can only be resolved in a particular set theory. No wonder Peter is so nervous about Russell's paradox, which has seemed like a non-issue for me for longer than I can remember. This semantical perspective seems to me to be slightly batty, frankly. The original set theorists wanted to make everything out of sets because they were concerned about establishing a consistent basis for mathematics. But that particular intellectual ambition, at least in the form that Frege and Russell and Hilbert had it, died over 50 years ago (murdered by Gödel). There really is no point in cleaving to set theory as some kind of intellectual bedrock these days. It is useful, and I don't mean to knock it, but it's just one ontology among many. I don't see any reason why OWL should be even slightly concerned with set theory of any description, be it naive, ZF or Aczelian. Of course, a MT will be described using set-theoretical language, but that's just because set-theoretical language is the common language of modern mathematics. I would be perfectly happy to couch the semantic meta-language in Aczel's set theory, but that would be controversial and there is really no need to, since once can get the same operational effect in conventional set theory by using an explicit extension mapping, as we did in the KIF and RDF MTs. This is merely a technical issue of mathematical style when writing MT documents. But the real issue is, should the ontologies be *about* set-theoretic constructions? Surely not. >I don't see any harm in continuing to talk naively about sets within OWL, as >long as we don't confuse what we are doing with actually replacing ZF. Why does OWL need to talk about sets at all? How many SW applications are likely to be about sets? Does anyone think that sets are the likely killer app that will revolutionize e-commerce? We seem to have been led into a blind alley here. >As I understand it, in a DL system with datatypes, the datatypes are >represented as some sort of oracle that is invoked when needed. I can >imagine a ZF oracle (hereafter ZFO) that logically corresponds to all purely >set-theoretic DAML+OIL statements that are consistent with a given knowledge >base. > >Thus in Peter's example, using my solipsistic reasoning and the oracle, > ><John, child, Joe>, ><Joe, rdf:type, Person>, >ZFO > |= > ><John, child, Joe>, ><Joe, rdf:type, Person> ><:_1, owl:onProperty, child>, ><:_1, owl:hasClass, Person> > (because this set does exist because ZFO sees that > its existence is consistent with the rest of the model) How does ZF produce RDF triples?? (I shouldn't ask, really, but I can't help it.) The trouble is that ZF will prove the existence of far more sets than you want. Most of the axioms of ZF assert the existence of sets, and together they assert a lot of existing. It is provable in ZF that any set conumerate with any subset of the integers exists, for example. It is provable that transfinite cardinals exist, and that the class of all points in any topological space exist, and that the class of all classes that are in 1:1 correspondence with their own power sets exists, and so on. It can do all that just starting from the empty set, all by itself. How do you prevent ZFO from generating the entire set-theoretical universe every time you tell it that John is a person? Pat -- --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola, FL 32501 (850)202 4440 fax phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes
Received on Friday, 5 April 2002 16:53:38 UTC