NNIL-formulas revisited: universal models and finite model property
From MaRDI portal
Publication:6323203
DOI10.1093/LOGCOM/EXAA063arXiv1908.01635MaRDI QIDQ6323203
Dick H. J. de Jongh, Fan Yang, Julia Ilin
Publication date: 5 August 2019
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.
This page was built for publication: NNIL-formulas revisited: universal models and finite model property
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6323203)
