 In proof-theoretic semantics, proof systems of a suitable form are seen as providing a meaning theory, see the entry  proof-theoretic semantics.  In that spirit, Francez (2016) presents two natural deduction proof systems for a propositional language with negation and implication, one in which AT, AT′, BT, and BT′ are provable, and another one in which AT, AT′, and the following variations of Boethius’ theses are provable: