Explanation of 1-generic to prove undecidability of halting problem

Question

This question is about an answer in question

Are there any proofs the undecidability of the halting problem that does not depend on self-referencing or diagonalization ?

Bjørn Kjos-Hanssen answer states that:

You can first show that the halting problem (the set 0ドル'$) can be used to compute a set $G\subseteq\mathbb N$ that is 1-generic meaning that in a sense each $\Sigma^0_1$ fact about $G$ is decided by a finite prefix of $G$. Then it is easy to prove that such a set $G$ cannot be computable (i.e., decidable).

I have trouble understanding this sentence as I am new to forcing. For example, what does "finite prefix" mean here? Can someone explain this sentence? (I know what $\Sigma^0_1$ means.)

Can someone explain the general idea behind forcing? I am also looking for easy to read introductions articles and books about forcing.

edit: So, how can we prove that each $\Sigma_1^0$ fact about $G$ being decided by a finite prefix leads to the fact that $G$ cannot be computable?

• Kaveh: I edited the question to make it more interesting. I hope that I kept the original intention. Feel free to roll back or edit.

Answer 1

A finite prefix of $G$ is $G \cap \{0,1,\ldots n\}$ for some $n$. It is easier if you look at the characteristic function of $G$ which can we viewed as an infinite word in 2ドル^\omega$. Then a finite prefix is a finite initial part of $G$.

For forcing, there are many resources, depends on what you want to learn. A point to start is the Wikipedia pages and the references listed there: Forcing (set theory), Forcing (recursion theory). Timothy Chow's article A Beginner's Guide to Forcing is a good introduction.

• cody: While the links are relevant, they certainly do not give enough information to complete the proof outlined by Bjorn. In particular the page on Forcing and recursion theory is atrocious.
• Kaveh: @cody, that question was added after my answer. I answered what was originally asked. And I am not sure it is a good idea to give an introduction to forcing here when Tim has already written a very good and readable introduction to it. As I see it the OP in place of reading the easy to read reference he asked for wants us to explain it even simpler. Feel free to do so, but I am not sure I will.
• cody: I really like Tim's introduction! However he makes no no mention of 1-genericity or give any mention to computability, which is what I meant by "not enough information to complete the proof outline".
• Kaveh: @cody, OK, I will try to address that (I don't have much free time right now, and I am hoping that Tim himself or someone else (Josh, Andrej, Emil, ...) will answer it before I find time :).
• cody: Thanks! I'll admit that I am interested in the answer to this question as well.