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?
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?).