Can we have a consistent theory whose signature is $(=,\in, S, +, \times)$ standing for identity and membership binary relations and the successor total unary function, addition and multiplication total binary functions with the followings?


Define: $x=\emptyset \equiv\_{df} \not \exists y (y \in x)$ 


Add all axioms of first order identity theory and axioms ZFC and PA


Define recursively: 


$S\_0(\emptyset) = \emptyset$


$S\_{i+1} (\emptyset) = S(S\_i(\emptyset))$


Add the following inference $\omega$-rule:


if $\phi$ is a formula, then: 


From $\big{[} \text {For } i=0,1,2,3,....: \phi(S\_i(\emptyset)) \big{]}$ 


We infer: $\forall x (\phi(x))$


[EDIT] The above question has been answered by Noah Schweber to be inconsistent if we include arithmetical language in Replacement! A possible salvage is to only add the axioms of identity theory, Zermelo, PA and the omega inference rule, or add on top of those a restricted form of Replacement (to the language of set theory).



Can we blend ZFC with true arithmetic?
What you've written is a bit unclear.


If you *do not* extend the ZFC schemes to formulas involving the new signature, then the answer is **yes**: letting $N$ be the standard model of arithmetic, $M$ be some countable model of ZFC, and $f:N\rightarrow M$ bijective, we can "port over" the structure on $N$ to $M$ and get a model of the theory you want - the point being that the arithmetic part and the set-theoretic part don't interact at all, so it doesn't matter how we do this.


* More generally, we can always "paste together" two structures of the same cardinality; things only get interesting when we demand, in addition to some properties of each separate reduct, some properties of the *interaction between* the two parts of the desired whole.


Meanwhile, if you *do* extend the ZFC schemes to formulas involving the new signature, then the answer is **no**: consider the formula "contains $\emptyset$ and is closed under $S$." If the replacement scheme is extended to formulas involving $S$, the ZFC(S)-part proves that such a set exists, but such a set can't be any of the $S\_i(\emptyset)$s since ZFC forbids sets from being elements of themselves.


