Decidability Issues for Two-Variable Logics with Several Linear Orders

Author Emanuel Kieronski



PDF
Thumbnail PDF

File

LIPIcs.CSL.2011.337.pdf
  • Filesize: 0.71 MB
  • 15 pages

Document Identifiers

Author Details

Emanuel Kieronski

Cite AsGet BibTex

Emanuel Kieronski. Decidability Issues for Two-Variable Logics with Several Linear Orders. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 337-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
https://doi.org/10.4230/LIPIcs.CSL.2011.337

Abstract

We show that the satisfiability and the finite satisfiability problems for two-variable logic, FO2, over the class of structures with three linear orders, are undecidable. This sharpens an earlier result that FO2 with eight linear orders is undecidable. The theorem holds for a restricted case in which linear orders are the only non-unary relations. Recently, a contrasting result has been shown, that the finite satisfiability problem for FO2 with two linear orders and with no additional non-unary relations is decidable. We observe that our proof can be adapted to some interesting fragments of FO2, in particular it works for the two-variable guarded fragment, GF2, even if the order relations are used only as guards. Finally, we show that GF2 with an arbitrary number of linear orders which can be used only as guards becomes decidable if except linear orders only unary relations are allowed.
Keywords
  • two-variable logic
  • linear orders
  • guarded fragment
  • decidability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads