Re: Question on DL negation

On Mar 6, 2007, at 7:09 AM, Vaughan Pratt wrote:

> Bijan Parsia wrote:
>> On 5 Mar 2007, at 17:21, Vaughan Pratt wrote:
>>> Bijan Parsia wrote:
>>>> You can see by playing around with combinations of the role  
>>>> constructors the effects on complexity.
>>>> Remember that all this is just (a fragment of) FOL (well, except  
>>>> if you add transitive closure per se), so all the constructors  
>>>> are just normal propositional (for the most part) connectives on  
>>>> binary predicates.
>>>> Expressive role constructors are associated with propositional  
>>>> dynamic logic (and converse propositional dynamic logic).
>>>> It's also instructive to see how arbitrary concept negation is  
>>>> difficult. You can see in the tractable fragments document that  
>>>> most of them allow concept (i.e., restricted) disjointness:
>>>>     <http://www.cs.man.ac.uk/~ezolin/logic/complexity.html>
>>>
>>> The difficulty with negation arises when passing from predicates  
>>> to classes.
>> I don't see that at all. I'm not sure what you mean by  
>> "predicates" and "classes" here. In DLs, classes generally refer  
>> to one place predicates (consider the obvious model theoretic  
>> intepretation).
>
> That's quite reasonable provided you're talking about some other  
> framework than OWL, e.g. the sets and classes of Goedel-Bernays set  
> theory.

OWL Full or OWL DL? In OWL DL, classes are *just* normal first order  
1 place predicates. Description logics are (by and large) notational  
variants of propositional (multi)modal logics which are, by the so  
called standard translation, fragments of first order logic. That was  
the context of this discussion.

> To quote from section 3, Classes, in the OWL reference manual at  
> http://www.w3.org/TR/owl-ref/,
>
>> every OWL class is associated with a set of individuals, called  
>> the class extension
>
> Not every predicate has a class extension in that sense, for  
> example the predicate true(x).

But this is not expressible in OWL DL...i.e., in (a fragment of)  
first order predicate logic.

> There is no "set of everything."  In contrast its negation the  
> predicate false(x) does have an extension, namely the empty set.
>
>>> The negation of a predicate simply complements its truth value.
>> Er... \forall(x)(C(x) \leftarrow \neg D(x)).
>> The predicate doesn't have a truth value.
>
> Ok, I start to see why you're having difficulty understanding me.   
> If you insist that a predicate such as D(x) does not have a truth  
> value at each x

I see why you are having true. I didn't say *that*. Of course when  
you instantiate it, it has a truth value. That will vary from model  
to model (typically).

> then it's easy to see we're going to be talking at cross purposes.   
> My reading of your example is that whenever C holds of x, D does  
> not, verified formally by taking the truth value of D at x,  
> negating it, and verifying that the resulting truth value is  
> *true*. Your reading may well be different, but in that case I'd be  
> very interested in seeing it.
>
> The fact that the truth value of D(x) depends on x doesn't mean  
> that it doesn't have a truth value, it just means that it has a  
> dependent truth value.

How is this talk helpful? In a standard model theory, the  
interpretation function won't map from a formulae C(x) to a truth  
value (but to a set of individuals).

>>>   Lifting logical connectives to the status of operations on sets  
>>> and classes is a delicate business.
>> I don't know why you put it this way. That is, I don't see any  
>> additional insight and some confusion. General negation is  
>> powerful and thus difficult. Having it allows for some nice  
>> interdefinability.
>
> If this is already adequately reflected in OWL's semantics of  
> negation then you're quite right that I'm wasting bandwidth  
> inappropriately by stepping in here.  However if it's not then it  
> seems to me that it is a potential future stumbling block for both  
> implementers and users.

OWL DL's negation is just classical first order logic's negation,  
with some restrictions on use. It has classical semantics. OWL DL  
properly includes normal truth functional sentential logic (for unary  
predicates). The standard connectives not, and, or, if, and iff are  
available and normally interdefinable (for the restricted class of  
formulae). There is *nothing tricky* going on.

>>> In the standard (Fischer-Ladner) semantics of propositional  
>>> dynamic logic, propositional negation of P is interpreted as the  
>>> complement of the set of worlds in which P holds *relative to* a  
>>> specified *set* W of all possible worlds constituting the  
>>> underlying set of the Kripke structure.  If your semantics has  
>>> that form then you are on safe ground with negation.  If however  
>>> it just has the intuitive meaning of "everything else" then you  
>>> leave yourself wide open to the problems of impredicativity such  
>>> as Russell's Paradox.
>> Uh, I'm very skeptical about this last bit, though I'm no PDL person.
>>     <http://www.springerlink.com/content/cf40guhq1m5t6lpu/>
>>     <http://www.sciencedirect.com/science? 
>> _ob=MImg&_imagekey=B6WJ0-4B55K9J- 
>> G-5&_cdi=6864&_user=494590&_orig=browse&_coverDate=04%2F30% 
>> 2F1979&_sk=999819997&view=c&wchp=dGLbVlb- 
>> zSkzS&md5=e6986bd20377ddee8f055be2886a8368&ie=/sdarticle.pdf>      
>> <http://www.csc.liv.ac.uk/~dirk/paper/mthesis-dirkwalther.pdf>
>> PDL with arbitrary negation of programs (i.e., arbitrary negation  
>> of role expressions) is undecidable, but that's hardly the same  
>> thing as allowing for paradoxes.  I'd be interested in your  
>> construction of the
>> Russell's paradox in PDL^-.
>
> Since my point was that you don't run afoul of Russell's paradox in  
> PDL with Kripke semantics, and you were the one who brought in  
> PDL^-, it would seem to me that whether or not it can be done in  
> PDL^- is for you to answer.

You claimed that there was some special sort of negation in PDL. The  
negation in PDL^- is, as far as I know, pretty much the same as in  
OWL DL. So if there is a trickiness or problem or potential Russell's  
paradox in OWL DL, it should show up in PDL^-. That's why I asked for  
a construction from you. The burden of proof is firmly on you to show  
that there is something weird or tricky about OWL DL's negation.

> That said, I'd be very interested to know whether anyone besides  
> you on this list proposes to apply to programs the same logical  
> connectives as are applied to propositions, especially the  
> nonmonotonic ones such as negation and implication.
[snip]

I don't know where you are getting that from. I'm not talking about  
any *nonmonotonic* negation or implication. And I'm not proposing it,  
I'm pointing out that that's how PDL works.

> For anyone who has been thinking along these lines, the paper  
> http://boole.stanford.edu/abstracts.html/#ActLog proposes one  
> approach to this that is very different from taking literally the  
> definition of a program as a set of behaviors and applying the  
> usual set-theoretic operations as done in the Walther thesis you  
> cited above.  With the exception of union, the set operations  
> applied to programs tend to be pretty incoherent, being heavily  
> dependent on the choice of notion of "behavior".  Union is an  
> exception because for all notions of behavior it simply aggregates  
> the behaviors, making the program A union B the nondeterministic  
> choice of A or B.
>
> Atomic negation, on the other hand, seems
>> ok. But restriction to atomic negation and restriction to  
>> disjointness are not quite the same thing.
>> Ok, this is a distraction now :)
>
> If negation in OWL is well in hand then I agree, and again I'm  
> sorry if I seemed to be butting in inappropriately.  If not then  
> I'm grateful for this opportunity to stir things up a little.

It's fine. It's just classical monontonic first order negation.  
Things are trickier in OWL Full *not* because of nonmon or what have  
you, but because it includes fairly strong reflection on its syntax.

Cheers,
Bijan.

Received on Wednesday, 7 March 2007 22:54:13 UTC