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?

  • 1
    $\begingroup$ 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! $\endgroup$ – Raphael Apr 13 '16 at 8:11
  • 2
    $\begingroup$ 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. $\endgroup$ – 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?).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.