most recent 30 from http://mathoverflow.net 2013-06-19T12:13:24Z http://mathoverflow.net/feeds/question/56728 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/56728/minimal-resources-for-undecidability-of-first-order-logic-the-number-of-variable boumol 2011-02-26T11:18:01Z 2011-02-26T11:18:01Z

<p>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]).</p> <p>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]). </p> <p>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]).</p> <p>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 <strong>question</strong> is the following.</p> <blockquote> <p>Is it decidable or undecidable $FO^3$ (without equality) in the case of the vocabulary which only has one binary predicate symbol?</p> </blockquote> <p>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).</p> <p>REFERENCES</p> <p>[1] The classical decision problem. Egon Börger,Erich Grädel,Yuri Gurevich. <a href="http://books.google.com/books?id=3po2Tv_UVcMC" rel="nofollow">http://books.google.com/books?id=3po2Tv_UVcMC</a> </p> <p>[2] A decision method for validity of sentences in two variables. Danna Scott. Journal SYmbolic Logic, 1962, 27, p. 477</p>