Can essential uniqueness justify introducing new constants in a formal system?

Question

Can a positive answer please refer to an elementary exposition, presumably stated in terms of conservative extension of the system with new constants and related axioms? I have not seen this anywhere.

A motivation for this question is the connection between the natural numbers and the classic Peano axioms (with second-order induction). The Peano axioms define a structure with a first element (taken by convention as 0 or 1) and one operation commonly known as "successor", and satisfying the axioms.

There are many instances of this structure, but any two of them are isomorphic (with respect to the constant (zero/one) and operation (successor) of the structure). In fact, for instances of the natural numbers, there is exactly one such isomorphism.

Many structures do not have essentially unique instances -- for example the group structure has many instances with varying properties. So formal statements about groups have forms such as "if g is a group, then . . . ".

It is straightforward to define a structure for the natural numbers, but it is not customary to write "if NN is an instance of the structure defined by the Peano axioms, then . . . ". In mathematical practice there is a constant symbol such as "N" for the natural numbers, "0" for zero, and perhaps "suc" for the successor function. The Peano axioms refer to those constant symbols.

Based on essential uniqueness, it seems to be formally justifiable to add the constants ("N", "0", and "suc") and the Peano axioms referring to them as a conservative extension to a suitable system. Aside from being (I believe) justifiable, this has the advantage of abstraction -- avoiding commitment to any specific instance of the natural numbers such as the von Neumann finite ordinals in set theory, which inevitably have additional properties specific to the instance.

The same approach should also apply to other essentially unique structures including the integers, reals, group(s) of size 2 and 3, and so on.

Answer 1

You seem to be asking the following question:

Given that the usual axioms of ($\mathrm{ZFC}$) Set Theory suffice to prove that (up to isomorphism) there is a unique model of the second-order Peano axioms, can we construct a conservative extension of ZFC in the language $\langle \in, \mathbb{N}, 0, S \rangle$ where $\mathbb{N}, 0, S$ are new constant symbols that satisfy the second-order Peano axioms?

This is possible. Constructions of this sort are known as "definitional extensions", and they always yield conservative extensions. The essential uniqueness does not really come into play. For an elementary exposition on definitional extensions of first-order theories, see e.g. Hajnal Andréka's lecture notes on definability.

---

I will sketch the construction of such an extension below. In what follows, let $\mathrm{PA_2}(N,z,s)$ abbreviate a first-order formula in the language $\langle \in \rangle$ of set theory that says "$N, z, S$ satisfy the nine axioms of second-order Peano arithmetic". This is a finite conjunction of sentences in the first-order $\langle \in \rangle$ language; moreover, $\mathrm{ZFC}$ proves $\exists N. \exists z. \exists s. \mathrm{PA_2}(N,z,s)$.

Take the theory $T$ in the language $\langle \in, \mathbb{N}, 0, S \rangle$ that has the following axioms:

1. the axioms of $\mathrm{ZFC}$ Set Theory, and
2. the axiom $\mathrm{PA}_2(\mathbb{N},0,S)$.

Consider any sentence $\psi$ that is provable in $\mathrm{T}$. Let $[\psi]$ denote the first-order formula obtained by replacing each occurrence of $\mathbb{N},0,1$ in the sentence $\psi$ with a respective fresh variable symbol $N,z,s$. It's clear that $\mathrm{ZFC}$ proves $\exists N. \exists z. \exists s. [\psi]$ for each axiom of $\mathrm{T}$ (and each axiom of classical logic). Moreover, if $\mathrm{ZFC}$ proves $[\varphi \rightarrow \psi]$ and $[\varphi]$, then $\mathrm{ZFC}$ also proves $[\psi]$. It immediately follows that if $T$ proves $\psi$, then $\mathrm{ZFC}$ proves the existential closure of $[\psi]$. Observe that if $\varphi$ is a ZFC-sentence, then $[\varphi] = \varphi$. Therefore, if $T$ proves $\varphi$ then $\mathrm{ZFC}$ proves $\varphi$, i.e. $T$ is conservative over $\mathrm{ZFC}$.