Two variable first-order logic over ordered domains

Journal of Symbolic Logic 66 (2):685-702 (2001)
  Copy   BIBTEX


The satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO 2 over ordered, respectively wellordered, domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially the same as for plain unconstrained FO 2 , namely non-deterministic exponential time. In contrast FO 2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings, wellorderings, or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO 2 and computation tree logic CTL



    Upload a copy of this work     Papers currently archived: 86,605

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

58 (#236,086)

6 months
1 (#874,758)

Historical graph of downloads
How can I increase my downloads?