It is well known that there is a fomula which means the consistency of PA in PA,that is Con(PA).
Then, Is Con(PA) true in standard model? or not?
Moreover,how to prove it?
I'm sorry. I edit this question as follows.
I can't understand well the relation of between [...is true in a relevant meta-theory] and [...is true in the standard model].
One requires a meta-theory to treat PA as object-theory.
Here, I adopt ZFC as meta-theory.
In ZFC, It is provable that PA has a model,and then Con(PA) is true.
On the other hand, it is said that Con(PA) is true in the standard model iff
Con(PA) is evaluated true at usual interpretation.
Above two notions slightly different (at least on definitions).
I can't understand well the relation of two notions - still after reading
Reese's answer.
Yes, provided $PA$ is consistent. $Con(PA)$ is just the statement "there is no proof of $1 = 0$ from $PA$". If it were not true, then there would be such a proof, and that proof would be coded by some standard natural number $n$. But then we could decode it back into the proof - here the standardness is important, because otherwise the "proof" might have nonstandard length and hence not be a real proof - and we then have a proof that $PA$ implies $1 = 0$. Since $PA$ proves $1 \neq 0$, this would make $PA$ inconsistent.