A Second-Order Logic in Which Variables Range over Relations with Complete First-Order Types
Alejandro L. Grosso, José María Turull-Torres · 2010
We introduce a restriction of second order logic, SOF, 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 SOFexistential fragment, Σ11,F, we can express rigidity, which cannot be expressed in SOω. We define the complexity class NPFby using a variation of the relational machine of S. Abiteboul and V. Vianu and we prove that this complexity class is captured by Σ11,F.