Re: Grist for layering discussion

From: Dan Connolly <connolly@w3.org>
Subject: Re: Grist for layering discussion
Date: 12 Jan 2002 10:09:11 -0600

> On Sat, 2002-01-12 at 05:43, Peter F. Patel-Schneider wrote:
> > From: Dan Connolly <connolly@w3.org>
> > Subject: Re: Grist for layering discussion
> > Date: 11 Jan 2002 20:46:44 -0600
> > 
> > > On Fri, 2002-01-11 at 19:14, Peter F. Patel-Schneider wrote:
> > > [...]
> > > > > So you feel that allowing reification -- or, presumably, allowing
> > > > > sets of statements as first class objects in the syntax -- makes the system
> > > > > such that one can necessarily deduce a contradiction from nothing?
> > > > > Then I need help understanding how.
> > > > 
> > > > Look at the spec for KIF at http://logic.stanford.edu/kif/dpans.html.  The
> > > > section on Metaknowledge has a nice description of one such problem.
> > > 
> > > A solved problem, no?
> > 
> > Well, yes, as long as you don't mind the effects of the solution, which are
> > to, roughly, disallow any ``formula'' that is self-referential.
> 
> Is that the case for the KIF v3 version of wtr too?

Using KIF v3 probably would probably allow positive self reference but not
negative self reference, getting you somewhat less than half the possible
self-referential formulae.

> I know the dpans KIF disallows any occurence of wtr inside wtr...
> but the v3 version didn't have that constraint; it just required
> that the not's be pushed out or something... I guess I should
> look it up...
> 
>   Changing Levels of Denotation
>   http://meta2.stanford.edu/kif/Hypertext/node35.html
> 
> So it's pushed in, not pushed out.

What matters is that the (meaning of the) sentence is changed.  This is not
a serious problem if all you care about is a WTR predicate that will only
be used in certain circumstances.  However, if you build your formalism
around syntactic structures that also have semantic meaning, then lots of
useful syntactic structures will probably be changed.  (Why probable?
Well, no one has gone ahead and done all the work to make this go through
for DAML+OIL, and the number of structures that have to be changed could
depend on the details.)  

> > Unfortunately, there are lots of such situations that are needed.
> > 
> > (In KIF, the problem only occurs with respect to WTR, because that is the
> > predicate that asks whether a ``list'' represents a true formulae.  In the
> > DAML+OIL case, however, there is essentially an implicit WTR attached to
> > every restriction.)
> 
> Really? can you elaborate?

Sure.

If you go ahead and make DAML+OIL compatible with the RDF model theory you
will have syntactic structures for each restriction (i.e., collections of
tuples) just as there is now.  The DAML+OIL model theory will also assign
class extensions to these syntactic structures, just as it does now.  So,
even now the DAML+OIL model theory takes syntactic structures
(restrictions), views them as something like formulae, and gives them the
equivalent of a truth value (class extension).

This is not so bad as long as you only have a limited number of
restrictions in your information bases.  However, to make entailment work,
all interpretations have to have the syntactic constructs for all (potential)
restrictions, which all have to be given a class extension.  The problem
arises when you want to give a class extension to the restriction that is
the set of all objects that don't belong to the restriction.  Thud!

> > > I've looked at it... several times. It seems to be exactly
> > > what we need. (Actually, the KIF v3 version is less constraining
> > > and looks more useful).
> > 
> > One way of translating the KIF solution to DAML+OIL would end up
> > disallowing classes from belonging to themselves, even indirectly.  I don't
> > think that you want that.
> 
> No..
> 
> Er... I meant to say that DAML+OIL/WebOnt could be based on
> KIF modified with the menzel indrection trick. I gather
> PatH is working on making this the standard model theory
> for KIF.

The indirection trick is only a way to allow having a class have itself as
a member.  It doesn't do anything directly to prevent paradoxes.  In fact,
it actually allows more paradoxes.


> > > But metaknowledge aside...
> > > 
> > > I'm still trying to figure out why the axiomatic semantics
> > > for DAML+OIL isn't perfectly good basis for WebOnt. It
> > > seems to play nicely with the RDF model theory, as far as
> > > I can tell. That is: the RDF model theory gives
> > > an n-triples document (and hence any RDF document)
> > > a meaning that corresponds
> > > directly to a KIF formula of the form
> > > 
> > > (exists (?x1 ?x2 ?x3)
> > >   (and
> > >     (p1 s1 o1)
> > >     (p2 ?x1 o2)
> > >     (?x3 s3 o3)
> > >     ...
> > >   )
> > > )
> > > 
> > > I trust you'll grant me that (PropertyValue p s o) isn't
> > > interestingly different from (p s o) with the menzel indirection trick,
> > > no?
> > > 
> > > What's wrong with specifying ont:complementOf ala:
> > > 
> > >  (forall (?C1 ?C2)
> > >   (iff (ont:complementOf ?C1 ?C2)
> > >        (forall (?x)
> > >          (iff (rdf:type ?x ?C1) (not (rdf:type ?x ?c2)))
> > >        ) ) )
> > > 
> > > How does the model theory paradox you presented earlier show
> > > up in an axiomatic specification like this?
> > 
> > You end up with an inconsistent axiomatization.  Not from things like the
> > above, of course, but from self-referential structures, in which you can,
> > roughly, say
> > 
> > 	if x belongs to y, then x does not belong to y
> > 	if x does not belong to y, then x does belong to y
> 
> Hmm... I don't quite follow.
> 
> If you have a few minutes to take that rough explanation and
> make it pricise/rigorous, I'd appreciate it.

Consider the restriction that I included in one of my posts of this week.

   _:1 a owl:Restriction .
   _:1 owl:onProperty rdf:type .
   _:1 owl:maxCardinalityQ 0 .
   _:1 owl:hasClassQ _:2 .
   _:2 oneOf _:3 .
   _:3 owl:first _:1 .
   _:3 owl:rest owl:nil .
   _:1 a _:1 .

An axiomatization should proceed as follows:

_:1 belongs to :_1
_:1 has no rdf:type relationship to { _:1 }
_:1 has no rdf:type relationship to _:1
_:1 does not belong to _:1

_:1 does not belong to :_1
_:1 has at least one rdf:type relationship to { _:1 }
_:1 has an rdf:type relationship to _:1
_:1 belongs to _:1

That wasn't hard, was it?  To make it rigourous, however, would require
devising a full axiomatization.  Any volunteers?

> > The problem with the current specifications of DAML+OIL, both the model
> > theory and the axiomatization, is that they don't work the same way as the
> > RDF model theory.
> 
> But suppose they did. i.e. look at KIF with a model theory
> similar to RDF's, where the relationship between
> properties and their extensions is indirect, and
> likewise for classes.
> 
> It seems to me that this would work.

Nope.  Indirection doesn't do anything for you here.

> >  This is fine, but then DAML+OIL and RDF(S) are different.
> > If you want this, then there is no problem, but you have lost the extension
> > relationship between RDFS and DAML+OIL.  
> > 
> > If making DAML+OIL (or OWL) an extension of RDF(S) is dropped from our list
> > of desirables, then there are lots of changes that I have to make DAML+OIL
> > (or OWL) better.
> > 
> > [...]
> > 
> > > > > > Why is there a problem?  The problem arises, as Pat has stated, from the
> > > > > > attempt to extend a representation formalism while not extending the
> > > > > > syntax.  This cannot be done in many circumstances and can only be easily
> > > > > > done in very limited circumstances.
> > > > > 
> > > > > I need to understand better where the problem lies.
> > > > 
> > > > Unfortunately, understanding the problem does require groking some
> > > > interesting logical notions.
> > > 
> > > I think I grok the relevant stuff... from what I can tell,
> > > you do have to be a bit careful, but it's not impossible.
> > > KIF's wtr is an example of a solution, no?
> > 
> > See above.
> > 
> > > i.e. TimBL's log:Truth is pretty much the same thing
> > > as KIF's wtr. And log:implies works sorta like:
> > > 
> > > (defrelation (log:implies ?P ?Q) <=>
> > >   (wtr '(implies ,?P ,?Q))
> > 
> > Well, not really.  If ?P or ?Q contain log:implies, the wtr solution will
> > certainly not be what you want.
> 
> Really?
> Why not? I'm using the KIF v3 version of wtr here.


> > As long as you can't create a contradiction, all this reification stuff
> > usually works fine.  However, contradictions and reification generally
> > allow you to create the Liar's paradox, and everything comes tumbling down.
> 
> Whenever I write down the Liar's paradox, TimBL usually counters
> with something about the excluded middle not applying... I agree
> that there's not much to talk about there until we figure out
> what we're using in place of the law of the excluded middle.

Yeah, if you want to throw out the law of the excluded middle, you really
need to tell me which of the at least 3027 (apparently) logics you are
using instead.


> -- 
> Dan Connolly, W3C http://www.w3.org/People/Connolly/
> 

peter

Received on Saturday, 12 January 2002 12:55:16 UTC