Re: A Single Foundational Logic for the Semantic Web

From: Sandro Hawke <sandro@w3.org>
Subject: Re: A Single Foundational Logic for the Semantic Web 
Date: Tue, 30 Apr 2002 07:06:43 -0400

> Peter F. Patel-Schneider writes:
> > [...]
> > Sandro Hawke writes:
> > > Perhaps I'm misreading it; if someone can present a
> > > paradox using only log:forSome, log:forAll, and log:implies, then I
> > > think I (and I'll venture TimBL and others) will be very interested.
> > > [Hrm, I guess you'll have trouble until an n3->n-triples conversion is
> > > written down.  It's in public e-mail between me and Tim; I'll dig it
> > > up if anyone seriously wants to try.  The idea is to use
> > > log:Conjunction and daml:List to assemble an n3 Formula.]
> > 
> > [...]
> > 
> > You have to be more precise here.  If *all* I can use is
> > log:forSome, log:forAll, and log:implies then I can't even make any
> > statement (because I don't have the . to finish the statement).

[...]

> > So, just what am I allowed to use?  What meaning am I to assign to the
> > semi-logical constants (like log:implies)?
> 

[Allowed: N-triples;
	  atomic formulae (reified triples), 
	  log:conjunction (of formulae, producing a formula),
	  log:implies between two formulae ]

All this more-or-less makes sense, and is non-controversial, aside from the
status of formulae as objects.  However, it does not get to propositional
Horn clauses, which allow for empty (false) conclusions.

>    (6,7): log:forSome and log:forAll, each of whose domain is a formula and
>   whose range is unlimitted.  These quantifiers act like this:  the triple
>            _:formula1 log:forAll _:var
>   is true if and only if _:formula1 would be true for any
>   consistant subsitution of _:var as an rdf:subject/predicate/object
>   in the formula.  More accurately, the substitution is of the object
>   denoted by _:var, not the identifier text itself, which is not
>   properly knowable, being syntactic rather than in the domain of
>   discourse.

Now here is the first problem.  What does it mean to do this substitution?
What happens if the ``variable'' occurs both as a subject/predicate/object
and as a formula.  It is perfectly legal rdf/n3 to have

    :v rdf:type rdf:Statement .
    :v rdf:subject :v .
    :v rdf:predicate :v .
    :v rdf:object :v .

> I think I need some clause about WFFs and self-reference, but I can't
> think of the right language.   Something like: all the predicates
> involving formulas are not defined for ill-formed or self-referencial
> formulas.  If that's where you want to push on the system, I'll try to
> be more precise.

Here is the second problem.  You are getting very close to

     If you come up with a problem, then I'm allowed to change my
     definitions so that it is no longer a problem.

This is *not* how the game is played.  In the game, *you* come up with a
set of statements/formulae/KBs and a way of given them meaning.  Then *I*
get to try to determine wether *your* definitions are consistent /
realizable.  (Logicians, of course, try to do this determination in
advance, just so that other logicians can't score off them. :-)

To have a defensible position *you* have to be completely clear,
particularly in this area, as it is the one where problems can and often do
arise.  If you are not clear, then *I* get to interpret your definitions in
any reasonable manner consistent with what *you* say.

[...]

> My focus here is on something closer to proper Horn clauses.  I'm
> using existentially quantified variables and allowing conjunctions in
> the consequent, instead of function terms and only an atomic sentence
> in the consequent, but I believe the forms are equivalent.
> 
>      -- sandro

The above is *much* less than in http://www.w3.org/2000/10/swap/log.n3.
I strongly suggest that whenever you are referring to this small language,
that it not be called n3 (with the logical additions) or Horn, as it is
much more limited than they are.  

Peter F. Patel-Schneider
Bell Labs Research

PS:  http://www.w3.org/2000/10/swap/log.n3 does't need log:notIncludes to
     suffer from the liar's paradox.  All it needs is a way of expressing a
     contradiction, which can come from log:equalTo with the intended
     meaning as given in the document.  (Note that ex:a log:equalTo ex:b is
     a contradition.)  Of course, the intended meaning of log:equalTo is
     not expressible in a logic without having something like a unique
     names assumption.  

PPS:  If you instead want to use domain equality, which is much more
      normal, then a contraction can obtained by using log:notEqualTo, as
      in ex:a log:notEqualTo ex:a .

Received on Tuesday, 30 April 2002 11:03:16 UTC