NNIL-formulas revisited: universal models and finite model property
Abstract
NNIL-formulas, introduced by Visser in 1983-1984 in a study of -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.
Cite
@article{arxiv.1908.01635,
title = {NNIL-formulas revisited: universal models and finite model property},
author = {Julia Ilin and Dick de Jongh and Fan Yang},
journal= {arXiv preprint arXiv:1908.01635},
year = {2020}
}