$\mathsf{fReR}_0$ is the set-theoretical system whose axioms consist of:
(1) Axiom of extensionality: $\forall z\in x\ (z\in y)\wedge\forall z\in y\ (z\in x)\rightarrow x=y$
(2) Axiom of empty set: $\varnothing\in\mathrm{V}$
(3) Axiom of pair set: $\{x,y\}\in\mathrm{V}$
(4) Axiom of union: $\bigcup x\in\mathrm{V}$
(5) Axiom schema of flat restricted replacement:
$\ \ \forall x\in a\ \exists!y\ (\phi(x,y)\wedge y\subseteq c)\rightarrow\{\ y\ |\ \exists x\in a\ (\phi(x,y)\wedge y\subseteq c)\ \}\in\mathrm{V}\ \ ,\ \ $where $\phi(x,y)$ is $\Delta_0$ .
It is easy to see that the following axiom schema can be proved in $\mathsf{fReR}_0$ :
$\Delta_0$-separation : $x\cap A\in\mathrm{V}\ \ ,\ \ $where $A$ is $\Delta_0$ .
Gandy [1] and Mathias [2] all assert (without proof) that the following statement can be proved in $\mathsf{fReR}_0$ :
$a\times b\in\mathrm{V}$
I don't think this assertion is trivial, moreover, I conjecture that it is false. I am based on the following observations:
(i) If we strengthen the axiom schema of flat restricted replacement to the following schema, then the existence of cartesian products follows trivially:
$\ \ \forall x_1\in a\ \forall x_2\in a\ \exists!y\ (\phi(x_1,x_2,y)\wedge y\subseteq c)\rightarrow\{\ y\ |\ \exists x_1\in a\ \exists x_2\in a\ (\phi(x_1,x_2,y)\wedge y\subseteq c)\ \}\in\mathrm{V}$ , where $\phi(x_1,x_2,y)$ is $\Delta_0$ .
Since we can form successively the sets $\{\{x_1,x_2\}\ |\ x_1\in a\wedge x_2\in a\}$ and $\{(x_1,x_2)\ |\ x_1\in a\wedge x_2\in a\}$ , and then form $a\times b$ .
(ii) Since there is only one variable $x$ range over $a$ in the original schema (of flat restricted replacement), I can only form the sets $\{\{x,z\}\ |\ x\in a\}$ and $\{(x,z)\ |\ x\in a\}$ , where $z$ is a parameter. This parameter can't be eliminated since I can't find a set $c$ (includes $a\times b$ ) in order to form $\{\{\{x,z\}\ |\ x\in a\}\ |\ z\in b\}$ .
My question is that whether the existence of the cartesian product of two sets can be proved in $\mathsf{fReR}_0$ .
References:
[1] R. O. Gandy, Set-theoretic functions for elementary syntax, in Proceedings of Symposia in Pure Mathematics, 13, Part II, ed. T. Jech, American Mathematical Society, 1974, 103–126.
[2] A. R. D. Mathias, Weak systems of Gandy, Jensen and Devlin, in Set Theory: Centre de Recerca Matematica, Barcelona 2003-4 , edited by Joan Bagaria and Stevo Todorcevic, Trends in Mathematics, Birkhauser Verlag, Basel, 2006, 149–224.
