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.
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.