First-Order Logic with Two Variables and Unary Temporal Logic

AbstractWe investigate the power of first-order logic with only two variables over ω-words and finite words, a logic denoted by FO2. We prove that FO2 can express precisely the same properties as linear temporal logic with only the unary temporal operators: “next,” “previously,” “sometime in the future,” and “sometime in the past,” a logic we denote by unary-TL Moreover, our translation from FO2 to unary-TL converts every FO2 formula to an equivalent unary-TL formula that is at most exponentially larger and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is essentially optimal. While satisfiability for full linear temporal logic, as well as for unary-TL, is known to be PSPACE-complete, we prove that satisfiability for FO2 is NEXP-complete, in sharp contrast to the fact that satisfiability for FO3 has nonelementary computational complexity. Our NEXP upper bound for FO2 satisfiability has the advantage of being in terms of the quantifier depth of the input formula. It is obtained using a small model property for FO2 of independent interest, namely, a satisfiable FO2 formula has a model whose size is at most exponential in the quantifier depth of the formula. Using our translation from FO2 to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types