 Whereas the basic ideas of connexive logic can be traced back to antiquity, the search for formal systems with connexive implication seems to have begun only in the 19th century in the work of H. MacColl (1878), see also Rahman and Redmond 2008. The basic idea of connexive implication was spelled out also by E. Nelson (1930), and a more recent formal study of systems of connexive logic started in the 1960s. In McCall 1966, S. McCall presented an axiomatization of a system of propositional connexive logic semantically introduced by Angell (1962) in terms of certain four-valued matrices. The language of McCall’s logic CC1 contains as primitive (notation adjusted) a unary connective ~ (negation) and the binary connectives ∧ (conjunction) and → (implication). Disjunction ∨ and equivalence ↔ are defined in the usual way. The schematic axioms and the rules of CC1 are as follows: