First-order definability of modal formulas: a simplified
proof of undecidability
Jeudi 6 novembre 2003 à 14 heures
Bureau 314 de l'Irit
Résumé : A new line of research
has appeared in the seventies, connected with the fact that modal formulas
can have a greater expressive power than classical first order ones. In this
respect, the modal formulas are usually divided in two classes: formulas
which are equivalent on Kripke frames to the conditions described by classical
first-order formulas (first order definable formulas) and formulas which
have no first-order equivalents. Thus the problem of deciding the first-order
definability of modal (and other non-classical) formulas has become more
and more examined. Its algorithmic solution was opened. In 1988 the lecturer
has proved that the problem of first-order definability is algorithmically
undecidable for intuitionistic formulas. From this, the undecidability of
first-order definability in the modal case follows easily, but the proof
was rather intricate and difficult of access for logicians which do not work
with intuitionistic formulas. In this lecture, a new simpler proof is
proposed.
Retour a la page des
seminaires