What is the simplest undecidable formula of the First Order Logic (Predicate Logic)?

Question

What is the simplest undecidable formula of the First Order Logic (Predicate Logic). I would like to get a practical feeling of undecidability. I am aware of the book http://www.springer.com/la/book/9783540423249 in which all the decidable un undecidable fragments of the first order logic are classified but instead of reading the whole book I would like to go straight to one, simple, undecidable formula and see where is the root cause of undecidability>

Answer 1

There is not one formula that is undecidable, unless you fix some kind of system that tries to decide formulas, and then it is possible that that formula will indeed stump that particular system.

That is: The undecidability of FOL means that relative to any one system that tries to figure out whether FOL formulas are valid or not, there will always be some formula that the system cannot decide on (assuming the system is sound and bound by the limits of Turing-computation)

But: for every one formula, there is some system that is able to say that it is valid or invalid. This is trivial: Relative to any one formula $\varphi$, consider two systems: system $A$ is a system that answer 'valid' whenever it receives $\varphi$ on the input, but for any other input doesn't give any decision. System $B$ is a system that answer 'invalid' whenever it receives $\varphi$ on the input, but for any other input doesn't give any decision. Now, given that $\varphi$ is either valid or invalid, one of these systems is sound, and makes the correct decision on $\varphi$. So, every one formula is decidable by some system.

So, to say that you have an undecidable formula only makes sense relative to a specific system: if you point to such a system (and again, assuming it is sound), then one could point to some formula that is undecidable for that system, but it is not true that there is some formula that is undecidable, period.

Still, many systems that try to figure out whether some FOL formula is valid or not are programmed using similar algorithms, and indeed many such systems will fail on just about invalid formula whose only counterexamples are of infinite size (indeed, very crudely, one aspect of the 'root' of the problem of undecidability is infinity ... that there are infinitely many possible scenarios to consider). Here is a fairly simple one:

$$\neg (\forall x\forall y\forall z((Rxy \land Ryz)\rightarrow Rxz)\land \forall x \neg Rxx \land \forall x \exists y Rxy)$$