Rigid First-Order Hybrid Logic

Hybrid logic is usually viewed as a variant of modal logicin which it is possible to refer to worlds. But when one moves beyondpropositional hybrid logic to first or higher-order hybrid logic, it becomesuseful to view it as a systematicmodal language of rigidification.Thekeypoint is this: @ can be used to rigidify not merely formulas, but othertypes of symbol as well. This idea was first explored in first-order hybridlogic (without function symbols) where @ was used to rigidify the first-order constants. It has since been used in hybrid type-theory: here oneonly has function symbols, but they are of every finite type, and @ canrigidify any of them. This paper fills the remaining gap: it introduces afirst-order hybrid language which handles function symbols, and allowspredicate symbols to be rigidified. The basic idea is straightforward, butthere is a slight complication: transferring information about rigiditybetween the level of terms and formulas. We develop a syntax to dealwith this, provide an axiomatization, and prove a strong completenessresult for a varying domain (actualist) semantics.