 Beside the systems mentioned, other intermediate systems between CK and C2 have been studied, in particular by proof theorists. Olivetti, Pozzato, and Schwind (2007) and Poggiolesi (2016) present sequent calculi for the systems CK, CK+ID, CK+SM and CK+SM+ID. Poggiolesi also investigates systems of natural deduction for the same systems.