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

TL;DR

This paper proves that the finite satisfiability problem for a specific fragment of two-variable first-order logic with a transitive relation is decidable, with complexity depending on the nature of the relation.

Contribution

It establishes the decidability and complexity bounds for the finite satisfiability problem in this logical fragment, extending understanding of logical decision problems.

Findings

Decidability of finite satisfiability for the logic with a transitive relation.

Complexity is triply exponential nondeterministic time.

Reduced complexity to doubly exponential when the relation is a partial order.

Abstract

We consider the two-variable fragment of first-order logic with one distinguished binary predicate constrained to be interpreted as a transitive relation. The finite satisfiability problem for this logic is shown to be decidable, in triply exponential non-deterministic time. The complexity falls to doubly exponential non-deterministic time if the distinguished binary predicate is constrained to be interpreted as a partial order.