# Recommendations for References on undecidability of First Order Logic

I am currently reading Computability and Logic by Boolos Burgess Geoffrey for the proof on "undecidability of first order logic". however, I find the notations a bit confusing. Can anyone recommend any resource website link/ video lecture or a book perhaps which will help me understand the proof of undecidability of first order logic? I am a CS student so, I do not want a completely mathematical /philosophical proof. I came across plenty of those on the web.

• I'm confused: you're asking for a non mathematical proof of a mathematical result?
– cody
Commented Dec 17, 2014 at 16:00
• I only asked for an "understandable proof" because I find it confusing to follow complicated mathematical proofs. Commented Dec 18, 2014 at 5:54

Let me clarify one subtle point: first order logic is only undecidable for certain given languages. In particular the language $\cal{L}$ that contains only monadic predicates, that is, predicates of the form $P(x)$ and no function symbols, is decidable.

If you allow function symbols or predicates with more than 1 argument, then $\cal{L}$ usually becomes undecidable. The proof involves encoding Turing machines and their computation sequences using the symbols of the logic. Then one adds a finite series of axioms $\phi_1,\ldots, \phi_n$, and build a formula $\psi(x,y)$ such that $$\phi_1,\ldots,\phi_n\vdash \psi(\overline{n},\overline{m})$$ is provable if and only if

The Turing machine with index $n$ halts in at most $m$ steps on the empty input.

Undecidability of FOL follows, as proving

$$\vdash \phi_1\wedge\ldots\wedge\phi_n\rightarrow \exists y,\psi(\overline{n},y)$$

is equivalent to determining wether the machine with index $n$ halts.

A detailed description of this proof is given in chapter 4 of Avigad's lecture notes on computability.

A Mathematical Introduction to Logic, Second Edition: Herbert B. Enderton