A Second-Order Logic in Which Variables Range over Relations with Complete First-Order Types

We introduce a restriction of second order logic, SO^F, for finite structures. In this restriction the quantifiers range over relation closed by the equivalence relation Ξ^FO. In this equivalence relation the equivalence classes are formed by k-tuples whose FO type is the same, for some integer k ≥ 1. This logic is a proper extension of SO^ω logic defined by A. Dawar. In the SO^F existential fragment, Σ₁^1,F, we can express rigidity, which cannot be expressed in SO^ω. We define the complexity class NP^F by using a variation of the relational machine of S. Abiteboul and V. Vianu and we prove that this complexity class is captured by Σ₁^1,F.