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?