 Alongside this ‘syntactic operation’ sense of connective—explained above for the primitive connectives and extended to derived connectives presently—another use of the term is indispensable: to refer to a connective with particular logical behaviour, as when people want to compare the behaviour of intuitionistic and classical implication. In due course we will see the notion of a consequence relation as one way of specifying such behaviour. If ⊢ is such a relation there is a unique language in the above sense which is the language of ⊢ and we can think of this ‘logically loaded’ sense of connective as applying to the ordered pair ⟨#, ⊢⟩; thus in the case of intuitionistic implication this would be ⟨→, ⊢I L⟩, where ⊢I L is the consequence relation of intuitionistic logic. (In fact it would be preferable to take equivalence classes of such pairs under a relation of translational equivalence but we will make no further explicit use of these ordered pairs or any such equivalence classes, and keep this aspect of the discussion relatively informal. Instead of saying “⟨#, ⊢⟩”, we will say things like “# as it behaves according to ⊢”. It would be better still to use not consequence relations—or the later introduced generalized consequence relations—as the second coordinate of the representatives ⟨#, ⊢⟩ but instead to insert here a reference to a proof system—a set of sequent-to-sequent rules of the kind introduced below, that is—since important differences between logics fail to show up at the level which would individuate them merely as consequence  relations.[1])