Natural deduction for first-order hybrid logic (Q1777372)

This paper is the first-order counterpart of the article ``Natural deduction for hybrid logic'' by the same author [J. Log. Comput. 14, 329--353 (2004; Zbl 1060.03036)]. In the present paper, a natural deduction calculus for first-order hybrid logic is studied. The underlying language is based on a multi-modal first-order language with identity and non-rigid designators and contains satisfaction operators \(a:\) as well as the hybrid binders \(\forall a\) and \(\downarrow a\), where \(a\) is any nominal. Also, geometric theories are taken into account. The results cover soundness, completeness and normalisation, as in the paper cited above. Finally, a Hilbert-style axiom system is introduced and proved to be sound and semantically complete.