Premium
The two‐variable fragment with counting and equivalence
Author(s) -
PrattHartmann Ian
Publication year - 2015
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.201400102
Subject(s) - undecidable problem , mathematics , fragment (logic) , satisfiability , stipulation , equivalence (formal languages) , logical equivalence , discrete mathematics , variable (mathematics) , boolean satisfiability problem , combinatorics , decidability , algorithm , mathematical analysis , law , political science
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 both NExpTime ‐complete. We further show that the corresponding problems for two‐variable first‐order logic with counting and two equivalences are both undecidable.