Least fixed points in Grzegorczyk's logic and in the intuitionistic propositional logic (Q1346913)

We study the definability of least fixed points for propositional positive schemes and \(\Pi\)-schemes in Kripke models. In an earlier paper [the author, Algebra Logika 31, No. 5, 493-498 (1992; Zbl 0795.03038)], it was shown that for \(\Sigma\)-schemes, the definability is a consequence of convergence in a finite number of steps. An example given there demonstrates, however, that \(\Pi\)-schemes may fail to meet this requirement, from which it follows that some other methods must be used to prove the definability for these schemes. Theorems for logics are obtained as corollaries.