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?