PA internal model Reviewing our current model theory course, I wondered why PA does not prove its own consistency (hopefully). I'll give a brief summary of the definitions and theorems I needed to get to the question, which will be a bit further down. This will contain a lot of bookkeeping since I do not see the problem in this argumentation, maybe an intermediate step is flawed.
Let's start with the language $\sigma = \{0, S\}$, the usual constant and successor function together with the axioms


*

*$\forall x:  Sx \not= 0$

*$\forall x, y: Sx = Sy \implies x = y$

*scheme f.a. $\varphi(x) \in FO_1(\sigma): \; (\varphi(0) \wedge (\forall x: \varphi(x) \implies \varphi(Sx))) \implies \forall x: \varphi(x)$
The usual Peano axioms in first order predicate logic. 
Say for a relation-symbol $R$ that $\Sigma(R) \subset FO_0(\tau \; \dot \cup \; \{R\})$ defines $R$ implicitly if for any new relation-symbol $R' \not \in \tau \; \dot \cup \; \{R\}$ it holds that $\Sigma(R) \; \cup \; \Sigma(R') \models \forall \overline{x}:(R\overline{x} \iff R'\overline{x})$, i.e. intuitively $R$ and $R'$ are the same.
Now Beth's definability theorem states that for each such implicitly definable $R$, there is also some $\psi(\overline{x}) \in FO(\tau)$ such that $\Sigma(R) \models \forall \overline{x}:(R\overline{x} \iff \psi(\overline{x}))$.
This leads to me believe that any primitive recursive function $f: \mathbb{N}^n \rightarrow \mathbb{N}$ is definable in $\sigma$ explicitly, i.e. by a closed formula $\varphi_f(\overline{x}) \in FO(\sigma)$ via its graph and an axiom asserting that the corresponding function symbol behaves correctly wrt. the graph.
Question: As I understand it, every discrete, countably infinite, linear order with a starting point can serve as a (standard-)model for PA as above, all being isomorphic to one another in the order-theoretic sense. Now take wlog. $\mathbb{N}$ and the primes $\mathbb{P}$. $\mathbb{P}$ as a unary relation is easily definable by $\chi(n) := \mathbb{P}n \iff \exists m: p(m) = n$ and $p$ being the function mapping a natural number k to the k'th prime ($p$ is primitive recursive, so definable by above). Now PA proves the trivially the following:


*

*There is a smallest prime, $SS0$

*There are infinitely many primes (and the order is linear and discrete)


I'd expect PA to prove the following also: If $\varphi(x) \in FO(\sigma)$ holds for $SS0$ and carries over by the "prime successor" $s_p$, mapping a prime to the next larger one (and all other to something arbitrary), than $\varphi(x)$ holds for each prime. But that would mean that PA $\vdash (\mathbb{P} \models$ PA$)$, which to me contradicts at least the 2nd Incompleteness Theorem by Gödel.
Can you point me to where I'm mistaken? Thought's I had on this matter, together with the reasons I don't believe they are applying here:


*

*Such a $\Sigma$ as above has to be finite, although this is not stated in our script. Then possibly the same argument would apply to these definitions as does apply to connectivity of graphs: $aCb \iff a=b \vee aEb \vee \exists c: (aEc \wedge cCb)$, which for a Graph $G=(V, E)$ is trivially modeled by $V^2$, allowing only overestimations, in my case useless.

*$\chi(n)$ as above has problems in non-standard models, however I think this can be fixed by something like $\forall a, b: a > b \implies \chi(a) > \chi(b)$, so no standard-non-primes will be the image of a non-standard number.

*PA somehow isn't able to "jump" via the induction over $s_p$ to the conclusion that some property holds for all elements in $\mathbb{P}$, however nebulous this seems to me.

*By allowing additional function-/ relationsymbols in the signature, the task to find an inner model for the less expressive theory becomes non-contradictory. However, I think since there are only finitely many new symbols used and by Beth's definability theorem, each can be defined by a (finite) formula, this all pieced together will produce only a single formula describing $\mathbb{P}$ relative to $\mathbb{N}$ uniquely in the signature $\sigma$.

 A: First of all, not every countable linear order is the order type of a model of $\sf PA$. In fact, we know there are exactly two order types of countable models of $\sf PA$: $\Bbb N$ and $\Bbb{N+Q\times Z}$.
Secondly, your proof is implicitly quantifying over formulas. What you proved is that $\Bbb P$ satisfies each of the [standard] axioms of $\sf PA$, but for $\sf PA$ to prove its own consistency you'd need to do more.
What does it mean for $\sf PA$ to prove its own consistency really? Well, it means that we code the language and the formulas into the natural numbers, and there is a recursively enumerable predicate $\tt PA$ which tells you when a number is a code of an axiom in $\sf PA$, and there is no internal proof, i.e. a code of a finite sequence of deductions, of contradiction from the numbers in these Gödel numbers.
But now when we look at the general situations we might have non-standard codes for axioms, and also non-standard codes for inference rules, and also codes of proofs whose length is non-standard. All of these things corresponds to "shadows" of real proofs with real inference rules from real axioms, and we can ignore them on the meta-level, but internally there is no distinction between them and the standard codes.
So what you proved is not very interesting, just that standard coded axioms hold somewhere. Which is true. But since internally $\tt PA$ might have more objects than the standard ones, you haven't proved that $\sf PA\vdash\rm Con({\tt PA})$.

Oh, also if you want to talk about first-order $\sf PA$, then you have to include $+$ and $\cdot$ in your language. It is not nearly enough to talk about $0$ and $S$. And if you remove the arithmetical symbols you either have to use second-order logic to define them, in which case your appeal to first-order model theoretic results is wrong; or you can end up with a complete and recursively enumerable theory, which cannot even internally first-order logic or even define the prime numbers (it can detect each standard prime separately, though).
