Well-quasi order on strictly positive formulas

We study the fragment of modal logic consisting of formulas constructed by a finite set of variables and constant ⊤ with connectives ∧ and ✸. This fragment is naturally orderedby implication in K4; we show that it is a well-quasi order and find upper and lower bounds for its ordinal type. We also show that the dual of any theory in this fragment has a finite number of axioms.