compactness - First-order Peano arithmetic and (the lack of) implicit definition of addition

I'm trying to show, through the existence of non-standard models of arithmetic, that the first-order Peano axioms (without those of multiplication) don't implicitly define addition in the sense of implicit definition as employed in the Beth definability theorem. I think I have it figured out, but am a bit unsure, and wanted to check if I am doing something misguided or wrong.

---

First, I'm understanding the relevant sense of implicit definition as follows:

Non-logical symbol $\alpha$ is implicitly definable in a theory $\Delta$ iff for all structures I and I' such that

1. I and I' simultaneously satisfy $\Delta$


2. domain of I = domain of I'


3. $I(\beta) = I'(\beta)$ for all non-logical symbols $\beta$ except for $\alpha$


4. $I(c) = I'(c)$ for every constant c

then $I(\alpha) = I'(\alpha)$ as well.

And the relevant Peano axioms are:

A1. (∀𝑥)𝑆(𝑥)≠0

A2. (∀𝑥)(∀𝑦)(𝑆(𝑥)=𝑆(𝑦)→𝑥=𝑦)

A3. (∀𝑥)+(𝑥,0)=𝑥

A4. (∀𝑥)(∀𝑦)+(𝑥,𝑆(𝑦))=𝑆(+(𝑥,𝑦))

---

Now, for the argument.

I know of the compactness argument that can be run to generate a non-standard number – call it 'a' – that is greater than any of the standard natural numbers (and brings along with an infinite number of successors and predecessors). Let's say we run this procedure to generate two other non-standard numbers, b and c, such that we have a set of standard and non-standard numbers that looks like:

0, 1, 2, 3, ... , a-2, a-1, a, a+1, a+2, ... , b-2, b-1, b, b+1, b+2, ..., c-2, c-1, c, c+1, c+2, ...

where the ellipses represent infinite descending and/or ascending chains of (non-)standard numbers. A2 will ensure that, a+0=a, b+0=b, and c+0=c. But what about, e.g., a+b?

I think you can run another compactness argument, as follows: Consider the following set of sentences, in the language consisting of the standard language of arithmetic together with the constant symbols 'a', 'b', and 'c' (but not written in strict first-order notation):

$\{\text{true sentences of arithmetic}\} \cup \{a≠0, a≠1, a≠2, ..., b≠0, b≠1, b≠2, ... , c≠0, c≠1, c≠2, ...\} \cup \{a≠b, a≠b+1, a≠b-1, a≠b+2, ..., a≠c, a≠c+1, a≠c-1, a≠c+2, ... , b≠c, b≠c+1, b≠c-1, b≠c+2, ...\} \cup \{a

If I'm thinking about this correctly, you can find a model of any finite subset of this union, and so by compactness can model the whole set (and a fortiori model the true sentences of arithmetic).

But, can we not also replace the last set of the union, with a set of sentences where all instances of 'c' are replaced by 'c+1' – i.e., $\{a+b=c+1, a+(b+1)=c+1+1, a+(b-1)=c+1-1, a+(b+2)=c+1+2, ...\}$ – and run an analogous compactness argument?

And if so, would we have shown that the Peano axioms don't (Beth) implicitly define '+' (as a+b=c in one case, and a+b=c+1 in the other, even though the domains are the same, and all other non-logical symbols are assigned the same values)? (I think I am a bit skeptical of this because I don't really understand how we individuate the non-standard numbers.)

I know there's a lot of sloppy text here, but any help would be greatly appreciated.

Thanks!