The Fluted Fragment with Transitive Relations

TL;DR

This paper investigates the satisfiability problem for the fluted fragment extended with transitive relations, revealing decidability in some cases and undecidability in others depending on the number of relations and presence of equality.

Contribution

It establishes decidability results for the fluted fragment with one transitive relation and equality, and undecidability results for the two-variable fragment with multiple transitive relations.

Findings

Finite model property holds with one transitive relation.

Finite model property is lost with multiple relations or equality.

Satisfiability is undecidable with three transitive relations or two plus equality.

Abstract

We study the satisfiability problem for the fluted fragment extended with transitive relations. The logic enjoys the finite model property when only one transitive relation is available and the finite model property is lost when additionally either equality or a second transitive relation is allowed. We show that the satisfiability problem for the fluted fragment with one transitive relation and equality remains decidable. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations (or two transitive relations and equality).