 The first completely rigorous definition of hybrid logic was given in Bull (1970), which appeared in a special issue of the journal Theoria in memory of Prior. Bull introduces a third sort of propositional symbols where a propositional symbol is assumed to be true exactly at one branch (“course of events”) in a branching time model. This idea of sorting propositional symbols according to restrictions on their interpretations has been developed further by a number of authors, see Section 5 of the paper Blackburn and Tzakova (1999) and also Blackburn and Goranko (2001).