Abstract: The finite-variable fragments of first-order logic have been widely studied in finite model theory over the past two decades. Restricting the number of variables makes first-order logic less expressive and often times allows for more efficient algorithms.

Two important examples of this behavior are model checking and equivalence testing. The model checking problem for first-order logic is PSPACE complete, but for any finite-variable fragment the problem becomes PTIME complete. The situation for equivalence testing (given two logical structures, is there a formula that is true for one of them and false for the other?) is similar. Equivalence testing for full first-order logic has the same complexity as graph isomorphism, but for any finite-variable fragment it is PTIME complete.

This talk will be a survey on several results on finite-variable logics, including the two problems mentioned above, and other connections to graph isomorphism.