[Top] [All Lists]

Re: [ontolog-forum] Is modal logic first-order?

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Thu, 22 Feb 2007 18:05:40 -0600
Message-id: <64412D8D-8C85-4075-B385-1F9110A2F2DB@xxxxxxxx>
On Feb 22, 2007, at 4:41 PM, Till Mossakowski wrote:    (01)

> During today's NIST-Ontolog-NCOR Mini-Series conference, there was
> a short discussion about whether modal logic with the usual
> Kripke semantics is first-order or not.
> Just to clarify the point:
> - in general, modal logic (let it be propositional or first-order  
> modal
>   logic) with Kripke semantics is of second-order nature.
> - more exotic modal logics may be truly second-order, like provability
>   logic obtained from Loeb's formula
>     Box (Box p -> p) -> Box p
>   The second-order nature comes in here, because the above formula
>   implicitly is universally quantified over p, but p is interpreted  
> as a
>   set of worlds - i.e. we have a second-order quantification.
> - For the usual systems like S4 or S5 etc. (S5 is used for DOLCE),  
> this
>   second-order quantification luckily is equivalent to a first-order
>   sentence. For example, the S4 axiom
>     Box p -> Box Box p
>   holds iff the accessibility relation is transitive, which is easily
>   expressed in first-order logic.
>   Hence, the second-order quantification can be eliminated and these
>   logics are of first-order nature.    (02)

Thanks Till for this clarification.  I'm afraid I muddied the waters  
by mis-hearing Michael's claim about the general stronger-than-first- 
order character of modal logic as *ruling out* the possibility of a  
truly first-order modal logic like S5 that is characterized by  
structures whose accessibility relations can be expressed by first- 
order conditions (so-called elementary structures).  General validity  
for arbitrary Kripke structures is certainly second-order, and many  
interesting and important modal logics require fully second-order  
conditions on accessibility, provability logics -- which Michael  
brought up in the telecon -- being a particularly important example.   
(If I recall correctly, Leob's formula above is only valid in  
structures in which accessibility is well-founded, which is of course  
well-known to be essentially second-order.)  My apologies for being  
less than clear on this point.    (03)

Chris Menzel    (04)

Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (05)

<Prev in Thread] Current Thread [Next in Thread>