The two‐variable fragment with counting and equivalence
Ian E. Pratt-Hartmann · Mathematical logic quarterly · 2015
We consider the two‐variable fragment of first‐order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are bothNExpTime‐complete. We further show that the corresponding problems for two‐variable first‐order logic with counting andtwoequivalences are both undecidable.