Repairing the Interpolation Theorem in First-Order Modal Logic

C. Areces, P. Blackburn, and M. Marx. Repairing the Interpolation Theorem in First-Order Modal Logic. In J. Halpern, editors, Proceedings of the 16th Annual IEEE Symp. on Logic in Computer Science, LICS 2001, IEEE Computer Society Press, 2001. Short Presentation

Download

[pdf] 

Abstract

Hybrid logics are extensions of orthodox modal logics in which it is possible to name worlds (or states, or times, ...). Such extensions have proved interesting for a number of reasons. We often want to reason about what happens at particular states, times, or locations, and this isn’t possible in orthodox modal logics. In addition, hybridization can improve the behavior of the underlying modal logic. For example, many modally undefinable properties (such as irreflexivity) are definable in hybrid logic, and general completeness and interpolation results can be obtained. Previous work has examined the effects of hybridizing propositional modal logics. But what happens when a first-order modal logic is hybridized? First-order modal logics are often badly behaved — does hybridization improve the situation? As far as interpolation is concerned, yes. As we shall see, hybridization allows us to repair failures of interpolation in first-order modal logic, in a very general way. This abstract is not self contained. For first-order modal logic (and in particular, a discussion of varying, expanding, contracting, and constant domains), see Fitting and Mendelsohn [4]. For Beth definability and Craig iterpolation, see Chang and Keisler [2]. As for hybrid logic, the most relevant points are the following. Hybrid logic contains special variables, written w, w0 , . . . , which range over worlds. Prefixing a formula by ↓w binds the variable w to the world of evaluation, while prefixing a formula by @w means that the formula should be evaluated at the state named by w. As the examples below show, it is the interplay between ↓w (“let w name the current state”) and @w (“evaluate at the state named by w”) that enable us to create interpolants so easily. For a detailed examination of \downarrow and @ in the propositional case, see Areces, Blackburn and Marx [1].

BibTeX

@InCollection{Areces2001e,
  author =       "C. Areces and P. Blackburn and M. Marx",
  booktitle =    "Proceedings of the 16th Annual IEEE Symp.\ on Logic in
                 Computer Science, {LICS} 2001",
  title =        "Repairing the Interpolation Theorem in First-Order
                 Modal Logic",
  year =         "2001",
  abstract =     "Hybrid logics are extensions of orthodox modal logics
                 in which it is possible to name worlds (or states, or
                 times, ...). Such extensions have proved interesting
                 for a number of reasons. We often want to reason about
                 what happens at particular states, times, or locations,
                 and this isn’t possible in orthodox modal logics. In
                 addition, hybridization can improve the behavior of the
                 underlying modal logic. For example, many modally
                 undefinable properties (such as irreflexivity) are
                 definable in hybrid logic, and general completeness and
                 interpolation results can be obtained. Previous work
                 has examined the effects of hybridizing propositional
                 modal logics. But what happens when a first-order modal
                 logic is hybridized? First-order modal logics are often
                 badly behaved — does hybridization improve the
                 situation? As far as interpolation is concerned, yes.
                 As we shall see, hybridization allows us to repair
                 failures of interpolation in first-order modal logic,
                 in a very general way. This abstract is not self
                 contained. For first-order modal logic (and in
                 particular, a discussion of varying, expanding,
                 contracting, and constant domains), see Fitting and
                 Mendelsohn [4]. For Beth definability and Craig
                 iterpolation, see Chang and Keisler [2]. As for hybrid
                 logic, the most relevant points are the following.
                 Hybrid logic contains special variables, written w, w0
                 , . . . , which range over worlds. Prefixing a formula
                 by ↓w binds the variable w to the world of
                 evaluation, while prefixing a formula by @w means that
                 the formula should be evaluated at the state named by
                 w. As the examples below show, it is the interplay
                 between ↓w (“let w name the current state”) and
                 @w (“evaluate at the state named by w”) that enable
                 us to create interpolants so easily. For a detailed
                 examination of \downarrow and @ in the propositional
                 case, see Areces, Blackburn and Marx [1].",
  editor =       "J. Halpern",
  note =         "Short Presentation",
  publisher =    "IEEE Computer Society Press",
  ISBN =         "978-0-7695-1281-5",
}