 where ≡ is classical equivalence. Since (A → B) ↔ ~(A → ~B) is a theorem of C and other connexive logics, the more problematic fact, from the point of view of this system, is the provability of (a). Pizzi and Williamson also show that in any normal system of consequential logic that contains BT, the formula (A → B) ≡ (A ≡ B) is provable if (A → B) ⊃ (A ⊃ B) is provable, in other words, consequential implication collapses into classical equivalence if (A → B) ⊃ (A ⊃ B) is provable. The construction of Aristotelian squares of opposition and their combination to Aristotelian cubes in systems of consequential implication is considered in Pizzi 2008. Two kinds of consequential implication are discussed and compared to each other in Pizzi 2018.