 The natural deduction proof system in Wansing 2016b can be seen a contribution to a bilateralist proof-theoretic semantics for certain connexive logics given in terms of provability as well as refutability conditions. In addition to a connexive implication that internalizes a notion of provability into the object language, there is also a connexive co-implication that internalizes a refutability relation. The resulting bi-connexive logic 2C is a connexive variant of the bi-intuitionistic logic 2Int from Wansing 2016a, 2018. A natural deduction calculus for a quantum logic satisfying Aristotle’s theses is presented in Kamide 2017.