I have asked this on the "computer science chat" ( vzn tried to explain me ) . I even watched a couple a videos to understand the theorem but still cannot convince myself. The following is the way the Godel's Incompleteness theorem is proved in Sipsers, where it is shown not all true statements are provable:

Notations, assumptions and preliminaries

  1. The statements being considered are assumed to be in prenex form ( with boolean operations $\neg,\vee,\wedge$ ). The model is $(\mathbb{N},+,*)$ ie. variables can take values from the set of natural numbers and relations are addition and multiplication. The set of true statements in this model is denoted by $Th(\mathbb{N},+,*)$. $Th(\mathbb{N},+,*)$ is shown to be undecidable by reducing $A_{TM}$ to it. The reduction is given as, on input $\langle M,w\rangle$ construct statement $\psi=\exists c [ \phi_{\langle M,w \rangle}]$, where, $\psi$ is true if and only if $c$ is an accepting computation history of string $w$ given as input to turing machine $M$.
  2. Proof of a statement $\phi$ is ( loosely speaking ), a sequence of statements, $S_1, S_2, . .. ,S_i$, where $S_i = \phi$. Each $S_i$ follows from the preceding statements and certain basic axioms about numbers, using simple and precise rules of implication. The proof a statement is denoted by $\pi$.
  3. The language $L=\{\langle \pi,\phi \rangle | \; \pi \text{ is a proof for } \phi \}$ is decidable ie. I can check the correctness of a proof for a statement. The Turing machine deciding $L$ is denoted by $D$.
  4. All provable statements are true.
  5. $P$ is a Turing machine that takes as input a statement $\phi$ tries to find a proof for it by giving $\langle \pi,\phi\rangle$ as input to $D$ for all proofs $\pi$ and accepting if $D$ accepts $\langle \pi,\phi\rangle$ for some $\pi$ ( if proof does not exist for $\phi$ $P$ does not halt ).


Construct the Turing machine $S$ such that
$S$ = "On input any input

  1. Obtain own description $\langle S \rangle $.
  2. Construct the statement $\psi=\neg \exists c [ \phi_{\langle S,0\rangle} ]$ ( $0$ is some specific input string ).

  3. Give statement $\psi$ as input to $P$.

  4. If preceding step accepts, accept. If it rejects reject. "

The reasoning given by Sipsers is if $P$ is able to find a proof for $\psi$ it means $S$ will accept $0$, but then statement $\psi$ will be false and a false statement can't have a proof which is a contradiction. The only option is that $P$ does not find a proof for $\psi$, but then $S$ won't halt on $0$ and $\psi$ becomes true. Thus $\psi$ is a true but unprovable statement.

My doubt is, isn't the reasoning given above that $\psi$ is true a proof in itself ? I expected the proof would be of sort where I am able to construct a statement $s$ and prove that neither $s$ nor $\neg s$ is provable. Am I misunderstanding something ? I can improve if my explanation of the problem is incorrect or vague.


In the proof $\phi_{\langle S,0 \rangle}$ is a formula with a single free variable $c$, such that the sentence $\exists c [\phi_{\langle S,0 \rangle}]$ is true if and only if there is an accepting computation history $c$ of input $0$ to Turing machine $S$.

  • 1
    $\begingroup$ The system can't prove "if ψ is false then ψ doesn't have a proof". ​ ​ $\endgroup$ – user12859 Nov 15 '15 at 20:43
  • $\begingroup$ This question belongs on math.se. $\endgroup$ – Yuval Filmus Nov 15 '15 at 21:39
  • $\begingroup$ @YuvalFilmus should I delete and repost on mathexchange ? $\endgroup$ – sashas Nov 15 '15 at 21:41
  • $\begingroup$ @sasha No, the moderators will migrate it there eventually. $\endgroup$ – Yuval Filmus Nov 15 '15 at 21:44
  • 2
    $\begingroup$ @YuvalFilmus This is at the edge between mathematical logic and computational logic. It's on-topic both here and on Mathematics. $\endgroup$ – Gilles Nov 15 '15 at 22:54

Your difficulties are hinting toward Gödel's second incompleteness theorem. The proof system $\Pi$ can formalize most steps in the proof, other than its own consistency – the fact that $\Pi$ cannot prove a statement and its negation. Following exactly this train of though, Gödel showed that a sufficiently strong proof system cannot prove its own consistency.

For more information, I suggest looking up resources on Gödel's second incompleteness theorem.

  • $\begingroup$ I don't come from a maths background. Could you point out resource(s) for a beginner ? I don't mind learning starting from the basics of mathematical logic. $\endgroup$ – sashas Nov 15 '15 at 23:07
  • $\begingroup$ Use your favorite search engine on the phrase "Gödel's second incompleteness theorem". There are many resources. $\endgroup$ – Yuval Filmus Nov 15 '15 at 23:11
  • $\begingroup$ @sasha : ​ ​ ​ Also, note that one can reach a stronger conclusion by replacing ​ "π ( if" ​ with ​ "π such that for all ρ, if ρ is shorter than π then D does not accept $\langle \hspace{-0.02 in}$ρ,¬φ$\hspace{-0.02 in}\rangle$ (if". ​ ​ ​ ​ ​ ​ ​ ​ $\endgroup$ – user12859 Nov 15 '15 at 23:26
  • $\begingroup$ @YuvalFilmus Sorry, but i would lastly like to ask that, the reasoning given that $\psi$ is true is indeed a proof but the proof can't be expressed as statements belonging to $Th(\mathbb{N},+,*)$. Am I understanding it correctly ? $\endgroup$ – sashas Nov 16 '15 at 3:53
  • 2
    $\begingroup$ @sasha Right, the proof is valid in the metalanguage but not in the language. The metalanguage knows (or rather assumes) that the language is consistent, but the language itself doesn't know it. $\endgroup$ – Yuval Filmus Nov 16 '15 at 6:11

This site is temporarily in read only mode and not accepting new answers.

Not the answer you're looking for? Browse other questions tagged .