Internalization: The case of hybrid logics (Q2772880)

The author presents a method of internalization for hybrid logic. It works in three steps. First the semantic theory of hybrid logic is formalized in a sequent calculus of predicate logic with additional axioms. In a second step a refined calculus with the subformula property is introduced which, however, is not fully internalized. This is solved in a third step by another calculus which uses a hybrid operator. In the final paragraph the author claims that the given strategy can be applied to a wide range of logical operations but that the exact limits of the method are still open.