 It is well-known that intuitionistic propositional logic can be faithfully embedded into the normal modal logic S4, which, like K, is based on classical propositional logic (cf. the entries  logic: intuitionistic  and  logic: modal).  There exists a translation γ, due to Gödel, such that a formula A  of intuitionistic logic is intuitionistically valid iff A’s γ-translation is valid in S4. In particular, intuitionistic implication is understood as strict material implication: γ(A → B) = □(γ(A) ⊃ γ(B)). Kamide and Wansing (2011) define a sequent calculus for connexive S4 based on MC. This system, CS4, is shown to be complete with respect to a relational possible worlds semantics. The proof uses a faithful embedding of CS4 into positive, negation-free S4. Moreover, it is shown that the cut-rule is an admissible rule in CS4 and that the constructive connexive logic C stand to CS4 as intuitionistic logic stands to S4. In the faithful embedding, the modal translation of negated implications is as expected: γ(~(A → B)) = □(γ(A) ⊃ γ(~B)). A similar translation is used in Odintsov and Wansing 2010 to embed C into a modal extension BS4 of Belnap and Dunn’s four-valued logic.