Can we make recursion into an axiom schema?

Question

The language of second-order arithmetic is (by definition) generated by a constant symbol $0$ and a unary function $S$. However, first-order arithmetic (hereafter $\mathrm{PA}$) famously requires a $+$ symbol and a $\times$ symbols.

Question. Can we eliminate the need to take $+$ and $\times$ as primitive in $\mathrm{PA}$, by replacing the "axiom schema of induction" with something stronger? I mean a schema guaranteeing that primitive recursion always defines a unique function.

I feel like this is impossible in a first-order language.

But if it is possible, it means we can define $+$ in the obvious way:

1. $\forall xy.(x+Sy) = S(x+y)$
2. $\forall x.x+0 = x$

Similarly with $\times$.

I know that PRA already does something like this, but that is much weaker than $\mathrm{PA}.$ I want something equal to $\mathrm{PA}$ in its power. I also don't want to start out with infinitely many function symbols like $\mathrm{PRA}$ does. Just $S$.

Answer 1

It is known that addition is not definable in the structure $(\mathbb{N},0,S)$ by any first-order formula. There is a sketch here. The same holds for multiplication, with a small variation of the proof.

That structure satisfies all true sentences of its language. So even if we took all those sentences as axioms, we still would not be able to define addition.

Answer 2

Let $\Sigma$ be the signature with a constant $0$ and a unary operation $S$ and let $(X, 0, S)$ be a $\Sigma$-structure. Fix a subset $\mathcal{F} \subseteq \coprod_{k \ge 0} (X^{X^k} \times X^{X^{2+k}})$ and say that $(X, 0, S)$ has primitive recursion with respect to $\mathcal{F}$ if, for every $(g, h) \in X^{X^k} \times X^{X^{2+k}}$, there is a unique $f : X^{1+k} \to X$ such that $f (0, \vec{x}) = g (\vec{x})$ and $f (S(t), \vec{x}) = g (t, f(t, \vec{x}), \vec{x})$.

Lemma. Let $k = 0$, let $g : X^0 \to X$ be given by $g () = 0$, and let $h : X^2 \to X$ be given by $h (t, y) = y$. If $(g, h) \in \mathcal{F}$ and $(X, 0, S)$ has primitive recursion with respect to $\mathcal{F}$, then $(X, 0, S)$ satisfies the second-order induction axiom (for unary predicates).

Proof. Let $P \subseteq X$ and define $f : X \to X$ by $f (x) = 0$ if $x \in P$ and $f (x) = 1$ if $x \notin P$. Suppose $0 \in P$ and for all $x \in P$, $S (x) \in P$. Then $f (0) = g ()$ and $f (S(t)) = f (t, p (t))$, so by hypothesis, $f$ must be the constant function with value $0$. Hence $P = X$, as required. 　◼

You might object that there is nothing that guarantees the existence of the function $f : X \to X$ constructed in the proof, but let us assume the metatheory lets us do that. Note that the functions $g : X^0 \to X$ and $h : X^2 \to X$ are definable in the $\Sigma$-language, and I imagine it is reasonable to assume that the primitive recursion scheme at least includes primitive recursion with respect to $\Sigma$-definable functions.

A more serious objection is that I have not specified what it means for a function $f : X^{1+k} \to X$ to exist in the first place. So perhaps one should also specify a subset $\mathcal{A} \subseteq \coprod_{k \ge 0} X^{X^k}$ of admissible functions or something like that. Then what we have starts to resemble Henkin semantics for second order logic.

Regardless, I think the moral is clear: in second order logic (with reasonable assumptions about the construction of predicates/functions), primitive recursion (in the sense above) is equivalent to the full induction principle. (To deal with $n$-ary predicates for $n > 1$, we need to assume a little bit more about $\mathcal{F}$.)