I'm interested in the strength of this theory, and in particular if it can be a theory in which all computer programming of mathematics (which I assume them to be ultra-finite proximate kinds of formalization since we cannot have an actual infinite set of inputs in actual computer programs) can be founded.
CONCRETE SET THEORY
language: first order logic with membership symbol added as a extra-logical primitive two place relation symbol $``\in"$, and another extra-logical primitive two place relation symbol of "equality" $``="$.
Extra-logical Axioms:
Equality axioms: $ x=x \\ x=y \to \forall a [x=a \to y=a] \\ x=y \to \forall a [x \in a \to y \in a] \\ x=y \to \forall a [a \in x \to a \in y]$
Membership axioms:
Extensionality: $\forall x,y [\forall z( z \in x \leftrightarrow z \in y) \to x=y]$
Concrete set construction: if $n=0,1,2,3,...$, then: $$\forall x_1,..,x_n \exists x \forall y (y \in x \leftrightarrow y=x_1 \lor ...\lor y=x_n)$$; is an axiom.