A uniquely defined function adds no old-language theorems

Explicit definitions are conservative: Adding relation symbols by old-language defining formulas and function symbols by old-language graphs that T proves uniquely total gives a conservative extension of T. The extension is equiconsistent with T. This includes any set of such definitions, since a proof uses only finitely many.

Robinson arithmetic, PA, and numeral conventions: Use the arithmetic signature $0,S,+,\cdot ,=$. Robinson arithmetic $Q$ consists of the universal closures of these seven formulas:

$Sx\mathrm{\ne }0;Sx=Sy\to x=y;x\mathrm{\ne }0\to \mathrm{\exists }yx=Sy;$ $x+0=x;x+Sy=S(x+y);x\cdot 0=0;x\cdot Sy=x\cdot y+x\mathrm{.}$

PA adds, for every formula $\varphi (x,\bar{z})$, the universal closure of $[\varphi (0,\bar{z})\wedge \mathrm{\forall }x(\varphi (x,\bar{z})\to \varphi (Sx,\bar{z}))]\to \mathrm{\forall }x\varphi (x,\bar{z})$. Parameters $\bar{z}$ are allowed. No induction schema is included in $Q$.

For an external natural number $n$, its numeral is the term $\bar{n}=S^{n}0$. Define $x\le y$ by $\mathrm{\exists }z(z+x=y)$ and $x<y$ by $x\le y\wedge x\mathrm{\ne }y$, with $z$ fresh. The left-addend witness is intentional: commutativity is not an axiom of Q.

Use def-set-coded-formal-derivation for the six logical schemes and three rules. Negation, conjunction and existential quantification are primitive: $A\to B$ expands to $\mathrm{\neg }(A\wedge \mathrm{\neg }B)$, $A\vee B$ to $\mathrm{\neg }(\mathrm{\neg }A\wedge \mathrm{\neg }B)$, and $\mathrm{\forall }xA$ to $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }A$. Inequality means negated equality. Substitute capture-free, always taking the least available fresh variable index and universally closing the remaining parameters in increasing index order. Thus each displayed axiom and each induction instance is a definite finite sentence.