It is known that adjunctive set theory interprets Robinson arithmetic, and that extensionality is not needed for that. (Montagna and Mancini, "A minimal predicative set theory", Notre Dame Journal of Formal Logic, 1994).
I wonder whether it is known if the following weak set theory (without extensionality) also interprets Robinson arithmetic. Axioms:
$\exists y\forall x(x\notin y)$
For every n, $\forall x_1\ldots\forall x_n\exists y\forall z(z\in y\leftrightarrow z=x_1 \vee \ldots\vee z=x_n)$
This theory was introduced by Vaught, and it does not interpret Robinson’s arithmetic. See Visser [1] for a thorough discussion of related theories; Vaught’s theory is denoted VS in the paper. (Note that the axioms are stated more concisely there: axiom 1 is a special case of axiom 2 for $n=0$.)
That VS does not interpret Robinson’s arithmetic Q follows by the following argument:
Q is finitely axiomatized. Thus, if it were interpretable in VS, it would be interpretable in its finite fragment.
VS is locally interpretable in the theory of nonsurjective pairing (using the obvious construction of $n$-tuples from pairs).
However, said theory of pairing is known to have decidable extensions, hence it does not interpret Q (or indeed, all of VS, which is also an essentially undecidable theory). Cf. Theorem 2 in [1,§3.2].
Reference:
[1] Albert Visser, Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), no. 4, pp. 299–326.
