Gödel's paradox: Why is "a proof that some universal statement is unprovable" not a valid proof that this statement is true? Here is a paradox I have some difficulty resolving:

As far as I understand, by one of Gödel's incompleteness theorems, in a first order logic theory with Peano arithmetic, one can find some non-trivial universal closed sentences (starting with a "for all" quantifier, all variables being bound) that can be proven to be unprovable.

Consider such an unprovable universal statement of the form "For all x, P(x)". We proved that there can be no counter example of this statement, exactly because finding such a counter example would disprove the statement hence contradicting Gödel's theorem which said that this statement can not be proven nor disproven. Therefore the given statement must be true.

As one can observe, my previous paragraph is a valid sequence of arguments that explain why my considered universal statement must be true. This previous paragraph is, by the very definition of proof, a proof of the given statement. My conclusion is that either Gödel was wrong, or mathematics are inconsistent :)

What is wrong with my reasoning ? Can you explain why the second paragraph would not be a valid proof? Does it have something to do with metalanguage? Even if metalanguage is mixed with regular language, cannot all the metalanguage used here be encoded in a first order logic with Peano arithmetic, and seen as not part of a stronger theory ?
The key step in your argument is when you say that if there is a counterexample to $\forall x.P(x)$, then the theory $T$ we speak about can prove that it is in fact a counterexample.

The particular form of $P(x)$ that comes out of Gödel's construction has the property that whenever we have a particular numeral $\bar n$, then the formula $P(\bar n)$ will always be true, and $T$ proves it to be true.

However, that does not constitute a proof of $\forall x.P(x)$. To think it does invokes a hidden assumption that everything our $\forall x$ ranges over can be expressed as a numeral. For sure this is true about our intended interpretation of $T$ as the "actual natural numbers", but in order for $T$ to prove something it needs not only to be true in the intended interpretation, but also in every other interpretation that satisfies the axioms of $T$.

Here the reasoning runs into trouble, because we know that $T$ must have some models where some of the elements don't correspond to numerals. (This is so independently of the incompleteness theorem; the "usual compactness argument" shows that such a model must exist for any theory that can speak about the naturals). Therefore, the known fact that $P$ is true and provable about all numerals doesn't imply that $\forall x.P(x)$ is true in all models, and therefore we can't conclude that it ought to be provable. And so the entire argument falls apart.



Gödel's notion of an "$\omega$-consistent" theory requires that there is no formula $\varphi(x)$ such that $T$ both proves $\varphi(\bar n)$ about every numeral, and proves $\exists x.\neg\varphi(x)$ which is the same as $\neg \forall x.\varphi(x)$. One way to show that a $T$ is $\omega$-consistent is to show that it has some model where all elements are numerals; interpreted in such a model the Gödel sentence will be true. The original incompleteness proof explicitly assumed that $T$ is $\omega$-consistent and used that to argue that $T$ cannot prove $\neg\forall x.P(x)$. Later, Rosser found a way to avoid this assumption and instead just assume that $T$ is consistent.
Your argument breaks down when you reason, that there is no counter example. There may be very well counter examples, but all we can reason is, that we are unable to construct one of them.