Re: DTTF: comprehension

From: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>
Subject: DTTF: comprehension
Date: Fri, 3 May 2002 10:52:10 +0100

[...]

> 3. Comprehension in Peter's proposal
> 
> Peter's proposal is something like
> 
> > If, however, the triples that are used to encode the syntax of the
> > constructs of the WebOnt language are unasserted, then these constructs do
> > not need to be part of the domain of discourse.  In this case, there is no
> > need for comprehension axioms, and a non-trivial theory can be developed for
> > the WebOnt language.
> 
> It is unclear whether "the triples that are used to encode" contains ones
> with properties such as rdf:type, rdfs:subPropertyOf ..., I certainly take
> it to mean all the owl:... ones.
> 
> However, there is still the problem of actually reasoning in OWL. A sound
> and complete OWL reasoner would be able to conclude that certain mainly dark
> syntactic expressions follow for all OWL interpretations.
> 
> e.g.
> 
> *empty*
> 
> entails
> 
> rdfs:subClassOf rdf:type |oneOf rdfs:subClassOf|

This is definitely a valid entailment.

> Peter has not clarified how given a new version of the Patel-Schneider
> paradox we would not have
> 
> *empty*
> 
> entails
> 
> Patel-Schneider-Paradox-Q

Well, this knowledge base is

_:1 owl:onProperty rdf:type .
_:1 owl:maxCardinality "0" .
_:1 owl:toClassQ :_2 .
_:2 owl:OneOf _:3 .
_:3 owl:first _:1 .
_:3 owl:rest owl:nil .

My proposal would have all these triples being dark.  Further, this
knowledge base has no semantic content, because all that it does is
``mention'' a restriction.  Therefore it follows from the empty knowledge
base, *but*, of course, it is not a paradox, as it has no semantic force.

> My previous understanding of Peter's position rested on there being a
> separate component, outside of OWL, that does set theoretic reasoning
> according to some well known set theory. 

This is a grave misunderstanding of my position.  You could think of my
position as a slight change to the standard view of description logics,
which has no more set theory than the RDF model theory does.

> This, on reflection, seems
> problematic since any such reasoner essentially embodies a set of
> comprehension principles and, given the real difficulty of some arcane
> aspects of set theory, the reasoner is not both sound and complete.

Not at all.  The reasoner does not need any comprehension principle.  It
just determines the meaning of a syntactic structure given to it.

[...]

> Conclusions:
> ============
> I think Pat and Peter exaggerate this issue.
> Finite set theory is trivial, countable set theory is not much harder.
> It's only when things get really big that life gets tough and we don't go
> there.

I don't see how set theory gets into the discussion at all.  I'm not
arguing for or against any particular version of set theory.

> Peter's proposal does not have explicit comprehension and does not help the
> implementator avoid paradox as a result.

Please provide some sort of evidence that my proposal has any paradox in
it.  I have not seen any such argument so far.

> In practice implementators will have comprehension rules, and it is a
> helpful clarification for us to specify them.

Implementors only need comprehension rules if comprehension rules are
needed.  My proposals do not require any comprehension rules, nor are
comprehension rules valid in my proposals, so I sure hope that implementors
of my proposals will *not* have comprehension rules.

peter

Received on Friday, 3 May 2002 12:00:39 UTC