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

Question

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

Proof

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.

EDIT

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

Answer 1

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.