Finite Satisfiability for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

Research output: Contribution to journalArticle


We consider two-variable, first-order logic in which a single distinguished predicate is required to be interpreted as a transitive relation. We show that the finite satisfiability problem for this logic is decidable in triply exponential non-deterministic time. Complexity falls to doubly exponential non-deterministic time if the transitive relation is constrained to be a partial order.

Bibliographical metadata

Original languageEnglish
Pages (from-to)218–248
Number of pages31
JournalMathematical Logic Quarterly
Issue number3
Early online date24 Jul 2018
Publication statusPublished - 3 Aug 2018

Related information


View all