NNIL公式再论：万有模型与有限模型性质
NNIL-formulas revisited: universal models and finite model property
摘要：
NNIL-公式是Visser在1983-1984年研究Heyting算术中的$Σ_1$ -置换时提出的，它是不允许蕴涵向左嵌套的直觉命题公式。Visser等人在1995年的一篇论文中得到了关于这些公式的第一个结果。特别地，证明了NNIL-公式恰好是Kripke模型的子模型下保持的公式。最近Bezhanishvili和de Jongh观察到NNIL公式也反映在Kripke模型的保色单调映射上。在本文中，我们首先展示了如何观察导致的结论，NNIL公式被保存的任意子结构不一定满足拓扑子帧条件。然后应用它构造了NNIL的万有模型。从这些万有模型的性质可以看出，NNIL-公式也正是保色单调映射所反映的公式。利用构造万有模型的方法，给出了由NNIL-公理化的逻辑具有有限模型性质的一个新的直接证明。
英文摘要：
NNIL-formulas, introduced by Visser in 1983-1984 in a study of $Σ_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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
