Intuitionistic Subframe Formulas, NNIL-Formulas and n-universal Models
Fan Yang

Abstract:
In this thesis, we investigate intuitionistic subframe formulas and
NNIL- formulas by using the technique of n-universal
models. Intuitionistic sub- frame formulas axiomatize subframe logics
which are intermediate logics characterized by a class of frames
closed under subframes. Zakharyaschev in- troduced the subframe
formulas by using [^,->]-formulas, which contain only ^ and -> as
connectives. It then follows that subframe logics are axiomatized by
[^,->]-formulas.

NNIL-formulas are the formulas that have No Nesting Of Implications to
the left. Visser, de Jongh, van Benthem and Renardel de Lavalette
proved that NNIL-formulas are exactly the formulas preserved under
taking submodels. The topic of this thesis was inspired by
N. Bezhanishvili who used the insight that NNIL-formulas are then
preserved under subframes as well to introduce subframe formulas in
the NNIL-form. It was proved that NNIL-formulas are su±cient to
axiomatize subframe logics.

This thesis is set up in a way to be able to connect the results on
subframe formulas defined by [^,->]-formulas and NNIL-formulas by
using n-universal models as a uniform method. Our original intention
to throw new light on subframe logics by the use of NNIL-formulas was
barely realized, but we do provide new insights on the NNIL-formulas
themselves.

Chapter 2 gives a background on intuitionistic propositional logic and
its Kripke, algebraic and topological semantics. In Chapter 3, we
discuss n-universal models U(n) of IPC by giving proofs of known
theorems in a uniform manner including a direct and very perspicuous
proof of the fact that the n-universal model of IPC is isomorphic to
the upper part of the n-Henkin model. This then also gives a method
for a new proof (Theorem 3.4.9) of Jankov's theorem on KC. In Chapter
4, we summarize classic and recent results on subframe logics and
subframe formulas. In Chapter 5, we investigate properties of the
[^,->]-fragment of IPC consisting of [^,->]- formulas only. This
chapter is based on the results in Diego, de Bruijn and Hendriks. We
redefined the exact model defined by using the n-universal models of
IPC and give a uniform treatment of known results.

In Chapter 6, we give an algorithm to translate every NNIL-formula to
a [^,->]-formula in such a way that they are equivalent on frames. We
study subsimulations between models and construct representative
models for equivalence classes of rooted generated submodels of U(n)
induced by two-way subsimulations. We construct finite n-universal
models U(n)^NNIL for NNIL-formulas with n variables by the
representative models and prove the related properties. As a
consequence, the theorem that formulas pre- served under
subsimulations are equivalent to NNIL-formulas becomes a natural
corollary of the properties of U(n)^NNIL. Finally, we obtain the
subframe logics axiomatized by two-variable NNIL-formulas by observ-
ing the structure of U(2)NNIL. Although it is not yet clear how to
general- ize the result for the model U(2)NNIL and the subframe logics
axiomatized by NNIL(p,q)-formulas to the models U(n)^NNIL for any n 2
->, this result clearly suggests that the U(n)^NNIL models are a good
tool for future work on subframe logics.