Variables

We consider the two-variable fragment of first-order logic, showing that it has the finite model property, and that its satisfiability problem is in NExpTime. We introduce the technique of reduction to the infinite tiling problem, and use it to show that the satisfiability and finite satisfiability problems for the three-variable fragment of first-order logic are both undecidable. We then introduce the technique of reduction to bounded tiling problems and use it to show that the satisfiability problem for the two-variable fragment of first-order logic is NExpTime-hard. We also consider the monadic fragment of first-order logic, and show that its satisfiability problem is also NExpTime-complete. Finally we obtain a semantic characterization of the expressive power of the k-variable fragment of first-order logic.