 Some of the most interesting (and problematic) aspects of Avicenna’s modal logic emerge in connection with the proofs used to establish the productivity of certain notable moods.  For instance, the controversial idea that the possible may be assumed to be actual in the context of a reductio proof (as well as in the proof of e-conversion of necessity propositions) is justified by intuitions that have sparked heated controversies in the post-Avicennan tradition (similar issues arise in the Greek tradition; for a philosophical interpretation of this technique, see Malink &amp; Rosen 2013). Another problem is the potential circularity of the proof of Barbara LML, which, even if we leave aside the issue of assuming the possible to be actual, seems to rest on Baroco LXL, which in turn depends on Barbara LML (Street 2002).