2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ I'm confused: you're asking for a non mathematical proof of a mathematical result? $\endgroup$ – cody Dec 17 '14 at 16:00
  • $\begingroup$ I only asked for an "understandable proof" because I find it confusing to follow complicated mathematical proofs. $\endgroup$ – GermanShepherd Dec 18 '14 at 5:54
2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.