 The strict implicational fragments of the logical systems S4 and S5 of modal logic are known as C4 and C5, respectively, and their Hilbert-style axiomatizations presuppose condensed detachment as their sole rule of inference. With insight from Kripke’s work, Anderson &amp; Belnap (1962) published the first axiomatization of C4 using the following 3-axiom basis, where the Polish notation ‘Cpq’ stands for ‘p → q’. 