RE: Still no paradox (was: Re: The Peter paradox isn't.)

>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