On the satisfiability problem for fragments of the two-variable logic with one transitive relation
share
We study the satisfiability problem for the two-variable first-order logic over structures with one transitive relation. decidable in 2-NExpTime for the fragment consisting of formulas where existential quantifiers are guarded by transitive atoms. As this fragment enjoys neither the finite model nor the tree model property, to show decidability we introduce novel model construction technique based on the infinite Ramsey theorem. We also point out why the technique is not sufficient to obtain decidability for the complimentary fragment where existential quantifiers are 'guarded' by negated transitive atoms, i.e. the existential subformulas are of the form ∃ y( Txy∧ Tyx ∧ϕ(x,y)), where T denotes the transitive relation. Hence, contrary to our previous claim, [31], the status of the satisfiability problem for the full two-variable logic with one transitive relation remains open.
READ FULL TEXT