SO F : a semantic restriction over second-order logic and its polynomial-time hierarchy

We introduce a restriction of second order logic, SOF, for finite structures. In this restriction the quantifiers range over relations closed by the equivalence relation ≡FO. In this equivalence relation the equivalence classes are formed by k-tuples whose First Order type is the same, for some integer k≥1. This logic is a proper extension of the logic SOω defined by A. Dawar and further studied by F. Ferrarotti and the second author. In the existential fragment of SOF, $\Sigma^{1,F}_1$ , we can express rigidity, which cannot be expressed in SOω. We define the complexity class NPF by using a variation of the relational machine of S. Abiteboul and V. Vianu (RMF) and we prove that this complexity class is captured by $\Sigma^{1,F}_1$ . Then we define an RMFk machine with a relational oracle and show the exact correspondence between prenex fragments of SOF and the levels of the PHF polynomial-time hierarchy.