It is well-known that First-Order Logic (FO) with a full vocabulary (i.e., a countable numbers of unary predicate symbols, a countable number of binary predicate symbols, etc.) is undecidable. And it is also known that the jump between decidability and undecidable occurs when we introduce binary symbols; i.e., FO is decidable in the case of the vocabulary with just a countable number of unary predicate symbols, and FO is undecidable in the case of the vocabulary which just one predicate symbol with arity $\geq 2$ (see the book [1]).

I stress that before (and also later) I am talking about the language without the equality symbol (but the previous claims are also true when there is an equality symbol, see also [1]).

Let us now look at FO (without equality) restricted to a finite number $k$ of variables (from now on $FO^{k}$). It is well-known that, with a full vocabulary, $FO^2$ is decidable [2] (the same was proved true by Mortimer when there is an equality symbol) while $FO^3$ is undecidable (see [1]).

My question concerns which is a minimal vocabulary to have undecidability for $FO^3$. In [1] it is proved that $FO^3$ is undecidable in the vocabulary which only has one binary predicate symbol and a countable number of unary predicate symbols. But I have not been able to find anything in the literature concerning the (un)decidability $FO^3$ when the vocabulary only has one binary predicate symbol. So, my **question** is the following.

Is it decidable or undecidable $FO^3$ (without equality) in the case of the vocabulary which only has one binary predicate symbol?

I would like to know whether there is a known answer to the previous question or whether this is nowadays considered an open problem (I would be really surprised if this is the case).

REFERENCES

[1] The classical decision problem. Egon Börger,Erich Grädel,Yuri Gurevich. http://books.google.com/books?id=3po2Tv_UVcMC

[2] A decision method for validity of sentences in two variables. Danna Scott. Journal SYmbolic Logic, 1962, 27, p. 477