 The paper Blackburn and ten Cate (2006) investigates orthodox proof-rules, which are proof-rules without side-conditions, and it is shown that if one requires extended completeness using pure formulas, then unorthodox proof-rules are indispensable in axiom systems for binder-free hybrid logic. However, in the case of the the stronger hybrid logic including the \(\mathtt{\downarrow}\) binder, an axiom system can be given that only involves orthodox proof-rules. See also the book Braüner (2011a) for another axiom system for hybrid logic as well as axiom systems for intuitionistic hybrid logic and a hybridization of Nelson’s paraconsistent logic N4 (compare to Costa and Martins (2017) where another paraconsistent hybrid logic is considered). A survey of intuitionistic hybrid logic can be found in Braüner (2011b).