Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.