Nehtdx

It is my understanding that Gödel's second incompleteness theorem says roughly that

there exists a sentence $varphi$ such that neither $varphi$ nor $negvarphi$ is provable in Peano's arithmetic. However one of them is true (in the structure $mathbbN$).

If $varphi$ is a formula in the style : "for all integers $n$, then $psi(n)$".
For me, if $varphi$ is false, proving it false is simply exhibing a counterexemple $n_f$ such that $negpsi(n_f)$. Therefore if it is false, then it must provably false, doesn't it?

Therefore, it someone manage to prove that it not provable, does it mean that $varphi$ must be true?

Is this reasoning correct?

No, because you may not be able to prove that the counterexample is false in Peano arithmetic. In other words, $negpsi(n_f)$ itself may be another statement that is true but not provable in PA.

However, if for every $n$, you know that either $psi(n)$ or $negpsi(n)$ is provable in Peano arithmetic, then your conclusion is correct. For example, this will be the case if $psi$ is quantifier-free, because then $psi$ is a Boolean combination of purely numerical statements like 2+2=4 and you can always prove or refute such a statement in Peano Arithmetic.

You are confusing theories and models. Theories are all the statements that are true given a number of axioms. Gödels incompleteness theorem deals with theories. A model is a mathematical structure that satisfies a theory. In a model every statement is either true or false and your counterexample idea would work, but that would only prove something for the model.

Consider groups for example. If we take the theory of group then we should not be able to prove $(forall x)(forall y)(xy=yx)$, i.e. every group is abelian as there exist abelian groups and non-abelian groups.

First of all, if I can prove that PA cannot prove $varphi$, that does not mean that $varphi$ is true ... for if $varphi$ is false, then of course PA will not be able to prove it. To give a concrete example: I can (well, a good mathematical logician better than I am can do this) prove that PA cannot prove that $1+1=3$ ... but obviously that does not mean that $1+1=3$

So, I think what you are trying to say is: If I can prove that PA cannot prove either $varphi$ or $neg varphi$, then that must mean that $varphi$ is true.

Second, your argument for this works when $varphi$ is of the form $forall x psi(x)$ where $psi(x)$ is quantifier-free, for if it is false, then $neg psi(n)$ is true for some $n$, and since PA can prove all quantifier-free truths expressed in the language of arithmetic, PA can prove this, and hence would be able to prove $neg varphi$, which goes against the assumption that PA could not prove this. So yes, your reasoning is correct .... for those kinds of statements $varphi$ ...

So, the question is: what kinds of interesting statements are there that contain a single quantifier, and for which you can prove that PA cannot prove either it or its negation?