On Feb 22, 2007, at 4:41 PM, Till Mossakowski wrote: (01)
> During today's NISTOntologNCOR MiniSeries conference, there was
> a short discussion about whether modal logic with the usual
> Kripke semantics is firstorder or not.
>
> Just to clarify the point:
>  in general, modal logic (let it be propositional or firstorder
> modal
> logic) with Kripke semantics is of secondorder nature.
>  more exotic modal logics may be truly secondorder, like provability
> logic obtained from Loeb's formula
> Box (Box p > p) > Box p
> The secondorder 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 secondorder quantification.
>  For the usual systems like S4 or S5 etc. (S5 is used for DOLCE),
> this
> secondorder quantification luckily is equivalent to a firstorder
> sentence. For example, the S4 axiom
> Box p > Box Box p
> holds iff the accessibility relation is transitive, which is easily
> expressed in firstorder logic.
> Hence, the secondorder quantification can be eliminated and these
> logics are of firstorder nature. (02)
Thanks Till for this clarification. I'm afraid I muddied the waters
by mishearing Michael's claim about the general strongerthanfirst
order character of modal logic as *ruling out* the possibility of a
truly firstorder modal logic like S5 that is characterized by
structures whose accessibility relations can be expressed by first
order conditions (socalled elementary structures). General validity
for arbitrary Kripke structures is certainly secondorder, and many
interesting and important modal logics require fully secondorder
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 wellfounded, which is of course
wellknown to be essentially secondorder.) My apologies for being
less than clear on this point. (03)
Chris Menzel (04)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (05)
