Proof Systems for Extensions of Hybrid Logic with Complex Terms
Andrzej Indrzejczak
University of Łódź
Abstract: Hybrid logic is a powerful extension of modal logic
which allows for internalization of essential semantical features in
the language. In particular, it leads to interesting results in proof
theory and provides suitable framework for dealing with several
intensional phenomena in natural languages. One of the specific
features of natural languages is a common use of complex names, like
definite descriptions, conveying information about their intended
designates. Since particularly interesting and difficult problems are
generated by their behavior in intensional contexts, it is important
to provide a suitable formal treatment in modal logic. We focus on
the development of well-behaved proof theoretic tools for dealing with
the iota (for complex terms) and lambda (for complex predicates)
operator in hybrid logic. Two such proof systems will be
discussed. The first was originally developed by Fitting and
Mendelsohn in the setting of standard modal logic and then
reformulated by AI in the setting of hybrid logic. The second was
developed by AI and Zawidzki on top of hybrid tableau system of
Blackburn and Marx.