<p>Let me clarify one subtle point: first order logic is only undecidable for certain given <em>languages</em>. In particular the language $\cal{L}$ that contains <strong>only monadic predicates</strong>, that is, predicates of the form $P(x)$ and no function symbols, is <a href="http://en.wikipedia.org/wiki/Monadic_predicate_calculus" rel="nofollow">decidable</a>.</p>

<p>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 <strong>finite</strong> 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 <em>provable</em> if and only if</p>

<blockquote>
  <p>The Turing machine with index $n$ halts in at most $m$ steps on the empty input.</p>
</blockquote>

<p>Undecidability of FOL follows, as proving</p>

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

<p>is equivalent to determining wether the machine with index $n$ halts.</p>

<p>A detailed description of this proof is given in chapter 4 of Avigad's <a href="http://www.andrew.cmu.edu/user/avigad/Teaching/candi_notes.pdf" rel="nofollow">lecture notes on computability</a>.</p>

CC BY-SA 3.0
2014-12-18T18:06:42.803Z
2014-12-18T18:06:42.803Z
cody
<p>A Mathematical Introduction to Logic, Second Edition: Herbert B. Enderton</p>

CC BY-SA 3.0
2014-12-15T22:53:02.937Z
2014-12-15T22:53:02.937Z
Flávio Botelho
<p>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.</p>

CC BY-SA 3.0
2014-12-17T16:00:40.287Z
I'm confused: you're asking for a *non mathematical* proof of a mathematical result?
cody
CC BY-SA 3.0
2014-12-18T05:54:43.090Z
I only asked for an "understandable proof" because I find it confusing to follow complicated mathematical proofs.
GermanShepherd
<lo.logic><undecidability>
Recommendations for References on undecidability of First Order Logic
GermanShepherd
# Recommendations for References on undecidability of First Order Logic

(Asked by: username_0 on 2014-12-15)

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.

**Tags:** lo.logic, undecidability
> **Comments:**
> **username_1**: I'm confused: you're asking for a *non mathematical* proof of a mathematical result?  
> **username_0**: I only asked for an "understandable proof" because I find it confusing to follow complicated mathematical proofs.  

---

## 2 answers

### Answer by username_1 on 2014-12-18. Score: 2 | Accepted answer

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](http://en.wikipedia.org/wiki/Monadic_predicate_calculus).

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](http://www.andrew.cmu.edu/user/avigad/Teaching/candi_notes.pdf).


---

### Answer by username_2 on 2014-12-15. Score: 1

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


---

