Successor axiom in Robinson arithmetic

Question

The successor axioms of Robinson Arithmetic (Q) are:

1. $\forall x\,(Sx\neq0)$

2. $\forall x\forall y\,[(Sx=Sy)\rightarrow x=y]$

3. $\forall y\,[y=0\;\lor\;\exists x\,(Sx=y)]$

Note that 3. differs from the following Successor Axiom of Peano Arithmetic:

4. $\forall x\exists y\,(y=Sx)$

Question: is there a proof in Q (in classical first-order logic with identity) of 4. ?

I take it that the canonical answer is "yes", since, e.g., Q is $\Sigma_1$ complete. But the only argument for this of which I am aware uses (instances of) induction in the metatheory. So, I wonder if one can actually point to a (first-order)) derivation in Q of 4.
If not, how, if at all, could a believer in Q, but no more, justify belief that every number has a successor?

Answer 1

Statement (4) is not an axiom of PA in any of its usual formulations, because it is not needed. Indeed, statement (4) is provable in first-order logic (with equality) from no axioms at all. By reflexivity of equality, $Sx=Sx$, from which you can deduce $\exists y(y=Sx)$ by existential introduction.

The point here is that merely having the symbol $S$ in your first-order language as a unary function symbol means that $S$ represents a function that can be applied to any element of your structure to obtain another element. This doesn't have to be stated as an axiom; it is implicit in the syntactic rules (specifically, the fact that for any term $x$, $Sx$ is a term).