What does Godels Incompleteness theorem "true but unprovable" mean?

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

• 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$.

• 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$.

• 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$.

• All provable statements are true.

• $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 ).

Proof

Construct the Turing machine $S$ such that

$S$ = "On input any input

• Obtain own description $\langle S \rangle $.

-

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.

StackExchange Computer Science Q#49529, answer score: 4