On two-variable first-order logic with a partial order

Abstract The main motivation for this work is the open question of decidability of the satisfiability problem for the two-variable fragment of first-order logic, ${\mathcal{FO}^{2}}$, with one transitive relation. In the presence of equality, the problem can be reduced to the corresponding problem when the transitive relation is required to be a strict partial order. It is known that its finite satisfiability problem is decidable but the decidability of the general satisfiability problem has been resolved only for restricted variants. More precisely, the problem is decidable for the fragment with comparable witnesses in which existential quantifiers are required to be guarded by atoms of the form $x<y$, a property in line with the standard translation of modal logic into first-order logic. We study two ‘complementary’ fragments: (i) the fragment with incomparable witnesses where formulas, when written in negation normal form, contain existential quantifiers applied only to conjunctions of the form $x \sim y\wedge \psi$, where $x\sim y$ means that $x$ and $y$ are not comparable by the order; and (ii) the fragment where both comparable and incomparable witnesses are allowed, but certain restrictions on the universal part apply. We show that ${\mathcal{FO}^{2}}$ with a partial order and incomparable witnesses is not locally finite. On the positive side, we show that the logic enjoys the finite antichain property that we believe is a crucial step towards showing decidability of its satisfiability problem. We also identify minimal syntactic restrictions on the universal part needed to retain the finite model property. These restrictions disallow statements of the form $\forall x,y (Ax \wedge By \rightarrow x \not \sim y)$, with distinct $A$ and $B$. Moreover, we show that with these restrictions in place the satisfiability problem for the fragment where both comparable and incomparable witnesses are allowed is decidable.