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