I am still struggling with the distinction between what is proven where. I think I have a good understanding of the theory and the meta-theory, but then I'm stumped every once in a while, so I fear there's something fundamental missing in my understanding.
By CON(PA) I mean the statement "PA is consistent" (meta-theory), whereas con(PA) is the sentence in the language of arithmetic expressing "there is no proof of a contradiction" (theory).
To cut to the chase, I wonder the following specifically: we know that con(PA) is really a number-theoretical statement, asking for the existence of a witness solving some Diophantine equation. By Goedel II, PA cannot prove con(PA) (unless it is inconsistent).
Now assume CON(PA) holds. Is it true that, for any $n$, PA proves $(*)$ "$n$ is not a code of a contradiction"? It is clear that PA cannot prove the universal closure of this (as then it would prove con(PA)).
This appears to be a theorem schema, where each $n$is an actual natural number (as defined in the meta-theory).
My reasoning is this: if there were $n$ such that PA did not prove $(*)$ then we'd have a model $M$ satisfying that $n^M$ is the code for a proof of an inconsistency. In the meta-theory, we could decode $n$ into an proof, which should now show that CON(PA) is false, a contradiction.
Surely it is not possible that this witness is non-standard? In other words, is it true that $n^M = n$ where the right hand $n$ is the actual natural as defined in the meta-theory? If not, that would be a problem to my reasoning as in such a case the witness would not decode to an actual proof in the meta-theory.
"$n$ is not a code of a contradiction" is doable: Gödel already gave us the tools to check whether something encodes e.g. an axiom or a proof and to perform this check within PA. It is also possible to additionally check if the last line of the proof encoded by $n$ is of the form $P\land \neg P$ where $P$ is a wff. Not only is the predicate "$n$ is not a proof of a contradiction" expressible in PA, it is also represented. So for any given $n$, provided that "$n$ is not the code of a contradiction" is true (which we assume as we assume CON(PA)), PA can prove it and could even put its finger on the line in the proof that is invalid.
Of course, if we assume $\neg$CON(PA), then PA will also prove that "$n$ is not the proof of a contradiction" ...