NP-Logic Systems and Model-Equivalence Reductions

In this paper we investigate the existence of model-equivalence reduction between NP-logic systems which are logic systems with model existence in NP. It is shown that among all NP-systems with model checking problem in NP, the existentially quantified propositional logic (彐PF) is maximal with respect to poly-time model-equivalent reduction. However,彐PF seems not a maximal NP-system in general because there exits an NP-system with model checking problem D^P-complete.