Algebraization of Hybrid Logic with Binders

Abstract. This paper introduces an algebraic semantics for hybrid logic with binders H(↓,@). It is known that this formalism is a modal counter-part of the bounded fragment of the first-order logic, studied by Feferman in the 1960’s. The algebraization process leads to an interesting class of boolean algebras with operators, called substitution-satisfaction algebras. We provide a representation theorem for these algebras and thus provide an algebraic proof of completeness of hybrid logic