# Showing that every satisfiable sentence with at most two variables has a finite model

I have tried to prove, in first order logic, that every satisfiable sentence (without function symbols) with at most two variables has a finite model. My attempts were unsuccessful.

This is an exercise from the (wider) model theory book written by Hodges (Encyclopedia of Mathematics and its Applications, Volume 42 - Model Theory, page 111). It follows an exercise about Immerman's pebble game, probably as an application.

It's easy to see that proving the following will suffice: (*) given a structure A, prove that for every number n, there is a finite structure B such that player II has a winning strategy in immerman's pebble game of length n with 2 pebbles (between A and B).

thanks for the help!

-
If you mention more about your attempts, you may find someone sympathetic enough to help. Although this is likely a graduate level problem, some might consider it not research level and close the question as being too localized. I hope that it stays open, especially if you provde more motivation and a reasonable summary of your attempts. Gerhard "Ask Me About System Design" Paseman, 2011.11.02 –  Gerhard Paseman Nov 2 '11 at 19:37
Also, it would help if you mention which language. I suspect there are counterexamples (Austin identities?) in second order logic. Gerhard "Ask Me About System Design" Paseman, 2011.11.02 –  Gerhard Paseman Nov 2 '11 at 19:39
The classical source to look for this kind of questions is the book "The Classical Decision Problem" by Borger-Gradel-Gurevich; I am sure there you can find a proof of this result. This particular result, when equality symbol is allowed, was firstly proved by Mortimer in his paper "On languages with two variables" (without equality symbol this was previously proved by Danna Scott in an abstract published at JSL). –  boumol Nov 2 '11 at 23:03
citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.9859 seems to have a proof, but the book recommended by boumol is probably better. As an aside, I'm not sure the exercises from Wilfrid Hodges' book are always to be solved. If I remember correctly, the Borel determinacy theorem is a subpart of an exercise in which he introduces Banach-Mazur games in his book 'Building Models by Games'. –  tci Nov 3 '11 at 0:06