0
$\begingroup$

I have been trying to wrap my head around this for a while now. Mostly by reading:

Logic in Computer Science - Modelling and Reasoning about Systems by Huth and Ryan.

But I'm just not getting it. I find their examples confusing. Nothing I have found on the web explains it clearly enough for me, so now I'm hoping someone here can educate me.

Thanks in advance for your time!

Edit 1: I have read theorem 2.22 and its 3 page long proof in Huth & Ryan several times. But there must be something shorter, something more to the core of the issue. Say that we can assume most of the "set up", like validity being undecidable and such. How would we then show that the satisfiability of the formula is undecidable?

$\endgroup$
4
  • $\begingroup$ Undecidability of FOL is a theorem: to "understand" it you need a proof of it. See Theorem 2.22 page 133 of Huth & Ryan. $\endgroup$ Oct 10, 2016 at 14:45
  • $\begingroup$ To understand the details, you have to master some of Computability theory where the basic result about undecidability are proved. Usually, the following results (like that regarding FOL) are proved reducing them to the "basic" one, i.e. finding a way to map e.g. the problem of "decidability about validity" to the undecidable computability problem. Thus, by contradiction, if the FIOL validity problem is decidable, we can apply the method to solve the "basic" problem; but we have prove that it is undecidable. Thus... $\endgroup$ Oct 10, 2016 at 14:49
  • $\begingroup$ @MauroALLEGRANZA Yes, I have read that theorem and its 3 page long proof. But there must be something shorter, something more to the core of the issue. Say that we can assume most of the "set up", like validity being undecidable and such. How would we then show that the satisfiability of the formula is undecidable? $\endgroup$
    – Skillzore
    Oct 10, 2016 at 18:07
  • $\begingroup$ There are different proofs, but they still require prerequisites; see e.g. Elliott Mendelson, Introduction to Mathematical Logic (6th ed 2015) : Proposition 3.54 (Church’s Theorem (1936)), page 225 : PF and PP are recursively undecidable. $\endgroup$ Oct 11, 2016 at 7:35

0

You must log in to answer this question.

Browse other questions tagged .