I am reading an interesting tutorial about FOL. In the tutorial, there is an exercise, which in my understanding, shows the incompleteness of the Peano system. The exercise can be expressed as a lemma: Let
\begin{equation} P_{1} \equiv \forall x \left(sx \neq 0\right), \end{equation}
\begin{equation} P_{2} \equiv \forall x \forall y \left(sx = s y \rightarrow x = y\right), \end{equation}
\begin{equation} P_{3} \equiv \forall x \left(x + 0 = x\right), \end{equation}
\begin{equation} P_{4} \equiv \forall x \forall y \left(x + sy = s \left(x + y\right)\right), \end{equation}
where $\equiv$ means identical in form when translated from metalanguage to object language. Then
\begin{equation} P_{1}, P_{2}, P_{3}, P_{4} \not\vDash \forall x \forall y \left(x + y = y + x\right). \end{equation}
This lemma basically says although commutative property can be proved at formal level, it is not a logical consequence in semantics. Thus, in my understanding, the proof of this lemma proves the incompleteness theorem.
Now the question is how to prove this lemma. Apparently, I need to find a structure $\mathcal{M}$ and an assignment $\sigma$ such that $\mathcal{M} \vDash P_{1}, P_{2}, P_{3}, P_{4} \left[\sigma\right]$ and $\mathcal{M} \not\vDash \forall x \forall y \left(x + y = y + x\right) \left[\sigma\right]$. As only sentences are involved, the only thing that matter is $\mathcal{M}$. Can somone provide thoughts on how to construct this $\mathcal{M}$?
HINT for constructing a countermodel: In order to satisfy PA1 and PA2 you need an infinite number of objects that can all be 'lined up' using the successor function (it's a good exercise to try and understand why this is so). Effectively, you are forced to have a bunch of objects that act like the natural numbers as part of your domain .. and so you may as well just say that the natural numbers are part of your domain, and you might as well say that the s and + functions work for the natural numbers like the normal successor and addition functions.
However, this does not prevent us to add further objects to that domain! Of course, once you add those other objects, you'll need to define how s and + will work on those other objects. So note: s and + can no longer be interpreted as the successor and addition function as we know them to work strictly on natural numbers. But hey, that's good, because that is of course your chance to ensure that + is no longer commutative! But whatever you do, be careful to make sure that with your definition/interpretation of the s and +, axioms PA1 through PA4 are still satisfied.