One of the strongest results on the decidability of theories is Rabin's Tree Theorem. One way to state it is the following: tThe problem of deciding whether a sentence on the monadic second order (MSO) theory of graphs has finite tree model is decidable. It is also well known that the complexity of such decision procedure is non-elementary (see Automata, Logics, and Infinite Games).
However, the non-elementary blow-up happens because in MSO logic we can define a partial order in the tree, which is impossible to do in first order logic. So, what is the complexity of deciding if a sentence in FO logic of graphs has a finite tree model? Do we know any upper/lower bounds? I have the feeling that it may just be in PSPACE, as the tree structure doesnt seem to allow to code much structure.
