There are several ways how to prove the completeness of this theory (let me call it $S$) without choice:

1. Prove in a purely syntactic way (by induction on the complexity of a formula) that $S$ has quantifier elimination.

2. Observe that $S$ has only one countable recursively saturated model.

   For an elementary version of this argument: expand $S$ to a theory $S'$ with countably many constants $\{c_n:n\in\omega\}$, and axioms that $c_n$ is not reachable from $c_m$ in finitely many steps for $n\ne m$. Using the compactness theorem, you easily show that if $\phi$ is consistent with $S$, it is consistent with $S'$, hence it holds in a countable model of $S'$ (this needs no choice as the language is countable). But reducts of countable models of $S'$ in the original language are all isomorphic (they consist of countably many copies of $(\mathbb Z,s)$).

3. Show that any two models of $S$ are elementarily equivalent by an Ehrenfeucht–Fraïssé argument.

4. The completeness of $S$ is an arithmetical ($\Pi_2$) statement. Thus, you can just prove the result in ZFC, and use the conservativity of ZFC over ZF for arithmetical sentences.

There are several ways how to prove the completeness of this theory (let me call it $S$) without choice:

1. Prove in a purely syntactic way (by induction on the complexity of a formula) that $S$ has quantifier elimination.

2. Observe that $S$ has only one countable recursively saturated model.

   For an elementary version of this argument: expand $S$ to a theory $S'$ with countably many constants $\{c_n:n\in\omega\}$, and axioms that $c_n$ is not reachable from $c_m$ in finitely many steps for $n\ne m$. Using the compactness theorem, you easily show that if $\phi$ is consistent with $S$, it is consistent with $S'$, hence it holds in a countable model of $S'$ (this needs no choice as the language is countable). But reducts of countable models of $S'$ in the original language are all isomorphic (they consist of countably many copies of $(\mathbb Z,s)$).

3. Show that any two models of $S$ are elementarily equivalent by an Ehrenfeucht–Fraïssé argument. Or, apply a ready-made EF argument: Gaifman's locality theorem.

4. The completeness of $S$ is an arithmetical ($\Pi_2$) statement. Thus, you can just prove the result in ZFC, and use the conservativity of ZFC over ZF for arithmetical sentences.

There are several ways how to prove the completeness of this theory (let me call it $S$) without choice:

1. Prove in a purely syntactic way (by induction on the complexity of a formula) that $S$ has quantifier elimination.

2. Expand the theory to a theory $S'$ with countably many constants $\{c_n:n\in\omega\}$, and axioms that $c_n$ is not reachable from $c_m$ in finitely many steps for $n\ne m$. Using the compactness theorem, you easily show that if $\phi$ is consistent with $S$, it is consistent with $S'$, hence it holds in a countable model of $S'$ (this needs no choice as the language is countable). But reducts of countable models of $S'$ in the original language are all isomorphic (they consist of countably many copies of $(\mathbb Z,s)$).

3. The completeness of $S$ is an arithmetical ($\Pi_2$) statement. Thus, you can just prove the result in ZFC, and use the conservativity of ZFC over ZF for arithmetical sentences.

There are several ways how to prove the completeness of this theory (let me call it $S$) without choice:

1. Prove in a purely syntactic way (by induction on the complexity of a formula) that $S$ has quantifier elimination.

2. Observe that $S$ has only one countable recursively saturated model.

   For an elementary version of this argument: expand $S$ to a theory $S'$ with countably many constants $\{c_n:n\in\omega\}$, and axioms that $c_n$ is not reachable from $c_m$ in finitely many steps for $n\ne m$. Using the compactness theorem, you easily show that if $\phi$ is consistent with $S$, it is consistent with $S'$, hence it holds in a countable model of $S'$ (this needs no choice as the language is countable). But reducts of countable models of $S'$ in the original language are all isomorphic (they consist of countably many copies of $(\mathbb Z,s)$).

3. Show that any two models of $S$ are elementarily equivalent by an Ehrenfeucht–Fraïssé argument.

4. The completeness of $S$ is an arithmetical ($\Pi_2$) statement. Thus, you can just prove the result in ZFC, and use the conservativity of ZFC over ZF for arithmetical sentences.