# Axioms - proof of halt

I am new to this forum and this is my first post. I am interested in solving a problem, but cannot find the way to think about it. If anyone can guide me through it, I would be obliged:

Let F be some system of axioms. You can assume F is sound (that is, it only proves true statements), and also that F is strong enough for Godel's Incompleteness Theorem to apply to it. Let G ( F ) be the mathematical encoding of "This sentence is not provable in F ." Also, let MF be a Turing machine that generates all possible F -proofs, one by one, and that halts if and only if it encounters a proof of G ( F ).

a) Does MF halt? Why or why not?

b) Is there a proof in F that MF halts, or a proof in F that MF does not halt? Why or why not?

• The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you!
– Raphael
Apr 13 '16 at 8:11
• What have you tried? Where did you get stuck? We do not want to just do your (home-)work for you; we want you to gain understanding. However, as it is we do not know what your underlying problem is, so we can not begin to help. See here for a relevant discussion. If you are uncertain how to improve your question, why not ask around in Computer Science Chat? You may also want to check out our reference questions.
– Raphael
Apr 13 '16 at 8:11

Let $CON(F)$ denote the sentence: "F is consistent".
You can prove $CON(F)\rightarrow \text{ MF does not halt}$, since if MF halts you have $F\vdash G(F)$ and thus by soundness $F\not\vdash G(F)$.
You cannot however, prove this unconditionally (unless your system is inconsistent), since this would mean $F\not\vdash G(F)$ which implies consistency (why?).