.png){kind=icon}
.png){kind=icon}
Return
On two-variable first-order logic with a partial order
.png){kind=icon}
PRE
AI
D
L
DOI：10.1093/logcom/exaf068.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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, FO2, 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 similar to y boolean AND psi, where x similar to y boolean AND 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 FO2 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 for all x, y(Ax boolean AND By -> x sic similar to 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 allo wed is decidable.
Keywords:
Two-variable first-order logic
satisfiability problem
decidability
finite model property
transitivity
partial order
finite antichains
locally finite order
Journal
J
IF:
0
Papers:
44
Citations:
0
Organization
Cited Papers