Re: Grist for layering discussion

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?

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.

> 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?

> > 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.

> > 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.

> 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.

>  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.

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

Received on Saturday, 12 January 2002 11:09:36 UTC