  Our paper is the first study of what one might call "reverse mathematics of
explicit fixpoints". We study two methods of constructing such fixpoints for
formulas whose principal connective is the intuitionistic Lewis arrow. Our main
motivation comes from metatheory of constructive arithmetic, but the systems in
question allows several natural semantics. The first of these methods, inspired
by de Jongh and Visser, turns out to yield a well-understood modal system. The
second one by de Jongh and Sambin, seemingly simpler, leads to a modal theory
that proves harder to axiomatize in an elegant way. Apart from showing that
both theories are incomparable, we axiomatize their join and investigate
several subtheories, whose axioms are obtained as fixpoints of simple formulas.
We also show that they are extension stable, that is, their validity in the
corresponding preservativity logic of a given arithmetical theory transfer to
its finite extensions.
