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

## TL;DR

This paper revisits NNIL-formulas, exploring their preservation properties under various model transformations, constructing universal models, and proving the finite model property for associated logics.

## Contribution

It introduces new preservation results for NNIL-formulas, constructs universal models, and provides a direct proof of the finite model property for NNIL-axiomatized logics.

## Key findings

- NNIL-formulas are preserved under arbitrary substructures.
- Universal models for NNIL are constructed.
- NNIL-axiomatized logics have the finite model property.

## Abstract

NNIL-formulas, introduced by Visser in 1983-1984 in a study of $\Sigma_1$-subsitutions in Heyting Arithmetic, are intuitionistic propositional formulas that does not allow nesting of implication to the left. The first results about these formulas were obtained in a paper of 1995 by Visser et al. In particular, it was shown that NNIL-formulas are exactly the formulas preserved under taking submodels of Kripke models. Recently Bezhanishvili and de Jongh observed that NNIL-formulas are also reflected by color-preserving monotonic maps of Kripke models. In the present paper, we first show how this observation leads to the conclusion that NNIL-formulas are preserved by arbitrary substructures not necessarily satisfying the topo-subframe condition. Then we apply it to construct universal models for NNIL. It follows from the properties of these universal models that NNIL-formulas are also exactly the formulas that are reflected by color-preserving monotonic maps. By using the method developed in constructing the universal models, we give a new direct proof that the logics axiomatized by NNIL-axioms have the finite model property.