Abstract

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.