Re: Question on DL negation

Bijan Parsia wrote:
>> 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.

According to 
http://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29 the 
negation connective of PDL applies only to propositions, not programs.

PDL's negation is a nonmonotonic (in fact antimonotonic) operation, in 
the sense that if p <= q then not-q <= not-p.  Similarly implication p 
-> q is nonmonotonic but not (purely) antimonotonic: it is antimonotonic 
in p and monotonic in q.

You may be thinking of nonmonotonic logics, where "nonmonotonic" refers 
to the deductive closure operation yielding the set of all consequences, 
not to the logical connectives.  Normally in logic, if a set G of 
formulas is a subset of a set G', the deductive closure of G is a subset 
of that of G'.  This does not hold in general in nonmonotonic logics, 
where deductive closure need be neither monotonic nor antimonotonic.

Vaughan

Received on Thursday, 8 March 2007 05:47:40 UTC