NNIL-formulas revisited: universal models and finite model property

Julia Ilin, Dick de Jongh, Fan Yang

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 im…