NNIL-formulas revisited: universal models and finite model property.

NNIL-formulas, introduced by Visser in 1983-1984 in a study of $\Sigma_1$-subsitutions in Heyting Arithmetic, are intuitionistic propositional formulas that do not allow nesting of implication to the left. The main results about these formulas were obtained in a paper of 1995 by Visser and others. It was shown that NNIL-formulas are exactly the formulas preserved under taking submodels of Kripke models. In the present paper an observation by Bezhanishvili and de Jongh of NNIL-formulas as the formulas backwards preserved by monotonic maps of Kripke models is applied to construct a universal model for NNIL. This universal model shows that NNIL-formulas are also exactly the ones that are backwards preserved by monotonic maps. The methods developed in constructing the universal model are used in this paper in a new direct proof that these logics have the finite model property.