Mfcttrf

The thing you're missing is that "true" and "false" are always relative to a model, but in arithmetic they are relative to the standard model, unless stated otherwise.

Now, if there is a counterexample to a $Pi_1$ statement, then it is a witness to its negation, a $Sigma_1$ statement. But here's the thing, $sf PA$ is $Sigma_1$-complete: every $Sigma_1$ statement which is true in $Bbb N$ is in fact provable from $sf PA$.

Now, if $forall xvarphi(x)$ is a $Pi_1$ statement which is neither provable nor disprovable from $sf PA$, that means that it is necessarily the case that $exists xlnotvarphi(x)$ is false (in $Bbb N$), otherwise, it would be provable. Therefore $forall xvarphi(x)$ is true (in $Bbb N$).

Some statements couldn't be refuted by presenting a counterexample, because that counterexample would itself be a universal claim. A counterexample to "all men are mortal" would be "nothing can kill Bob". In mathematics, it would be more like, "for any $xin S$, there is some $yin T$ such that..."

Let's discuss a concrete example. Write your favourite positive integer as a sum of powers of two, where the exponents are written in the same format etc. so no number $>2$ appears, e.g. $37$ becomes $2^2^2+1+2^2+1$. Now replace every $2$ with a $3$ and subtract one, viz. $3^3^3+1+3^3$. Now repeat moving $3$s to $4$s, viz. $4^4^4+1+3times 4^3+3times 4^2+3times 4+3$. The numbers grow very fast at first, but it can be shown in ZF, a version of set theory, that eventually you'll get to $0$. On the other hand, it can also be shown that the Peano axioms, the weakest system Gödel considered in his incompleteness theorems, can't prove this result.

What one can prove, in PA (and in fact in even weaker arithmetical theories than that) via a careful version of the argument you give is "If PA is consistent, then there is a statement $G$ such that $G$ holds and PA cannot prove $G$." If PA could prove its own consistency, then it would prove both $G$ and that PA cannot prove $G.$ Thus the latter is a false statement and PA is unsound. Thus if PA is sound, then it cannot prove its own consistency. This is essentially a proof of (a weak form of) the second incompleteness theorem from the first.

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.

Specifically, given a logic $L_1$, you can construct (algorithmically) a statement $P(x)$ such that there is a proof of $P(0)$ and there is a proof of $P(1)$ and there is a proof of $P(2)$, etc, but there is no proof of $forall k~P(k)$ (and all of that assumes consistency).

We proved that there can be no counter example of this statement

We have not formally proved this. There is no formal proof in $L_1$ that $lnot exists k ~ lnot P(k)$. To show $lnot exists k ~ lnot P(k)$, we actually need to use the assumption that $P(k)$ represents the statement "$k text is not a proof of G$" (for a specially chosen $G$). But that assumption isn't actually provable in $L_1$, it is just something we know to be true because it was designed that way.

My conclusion is that either Gödel was wrong, or mathematics are inconsistent

Godel wasn't wrong, nor is the logic the theorem deals with. The logic is just incomplete. And more importantly, it is incompletable.

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 ?

Yes, and there is huge branch of logic that deals with this approach. It is called provability logic: https://plato.stanford.edu/entries/logic-provability/ . But, even after you encode all the outer logic and use it as your new logic, then you've just created a new logic $L_2$, from which a new $P$ can be algorithmically constructed. No matter how much "meta" you keep adding, a new $P$ can be created.

I suggest reading through https://plato.stanford.edu/entries/goedel-incompleteness/ , it is an absolutely fantastic reference for Godel's first incompleteness theorem (but an unfortunately deficient reference for the second, that requires a bit more framework than the article presents).

I think people here understand the flaw in my argument so I will try to make it sound simple. To try to sum it up, I think the problem with my second paragraph, was that although it is indeed a proof of the universal statement, it is a proof assuming the statement itself, rather than just the principles of the implicit theory. It is perfectly circular in its form, it does not mean that the theory proves the statement. Just that the statement proves itself by virtue of it being true.

As one can notice "proof" is a relative notion. Unlike what I failed to realize early enough, one should always make the mental effort to ask oneself: proven with respect to what?

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, the 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.negvarphi(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 $negforall x.P(x)$. Later, Rosser found a way to avoid this assumption and instead just assume that $T$ is consistent.