Where could I find a discussion about "minimal sets" of axioms for ZF(C) set theory? I know ZF is not finitely axiomatizable so a "minimal set of axioms for ZF" is actually a minimal set of metaxioms (or axiom schemata) that quantify (in natural language) over well-formed-formulas of first order logic (with equality symbol), like separation or replacement.
EDIT: I want to read a discussion about "minimal sets" of axioms for ZF(C) set theory from these usual axioms which have a name. By a "minimal list" I mean a non-redundant axiomatics. An example of a list, in the usual ZFC formulations, the "minimal" axioms would be (1) extensionality, (2) union, (3) pair, (4) infinity, (5) substitution, (6) choice. Separation and power come out with (6), the empty comes out via separation. Another list is Bourbaki's. A Professor of mine said me that "He [Bourbaki] has a very nice formulation that uses (1) extensionality, (2) pair, (3) parts, (4) infinity, (5) separation and union (in a single axiom, but I count two axioms for my purposes). It is well known that he did not use the axiom of choice (AC) because using Hilbert's epsilon (his famous "tau") allows him to demonstrate AC".
My purpose is didactic. I am seeking some lists like that and the discussions of preferring some above others.
 A: The earliest serious result in this direction I know is due to Levy. Levy showed that the seemingly-weak theory $$\mbox{$T_0=$ Z + $parameter$-$free$ replacement}$$ proves full replacement.
Levy, and later (and some unintentional overlap) Schindler and Schlicht, looked at axiomatizations of ZF (and related) which avoid using parameters in the separation/replacement schemes. (Levy's paper is in the somewhat-hard-to-get-hold-of Tarski symposium proceedings, and I don't think there's an online version.)
Moving forward, I think some of Harvey Friedman's work addresses this problem - see e.g. this paper of his.

On the other hand, I believe Mostowski showed that any c.e. axiomatization of ZF (or similar) has a proper c.e. sub-axiomatization (the c.e. requirement is actually WLOG; given a proper sub-axiomatization $Y$ of $X$, fix $y\in X\setminus Y$ and let $Y'=X\setminus\{y\}$). So this rules out the existence of any truly minimal axiomatization. But I can't find a  source for this or prove it on my own at the moment, so take this with a grain of salt.
A: Let $\mathsf{\in}$ be a binary predicate. Let $\mathsf{W}$ be a constant. Define the following axiom schemas:
Subworld separation ($\mathsf{SS}$):
$$\mathsf{(\forall x \in W) (\exists y \in W) (\forall z) (z \in y \leftrightarrow (z \in x \land \phi))}$$
where $\mathsf{\phi}$ is a formula in $\mathsf{L(\in, W)}$ where $\mathsf{y}$ is not free.
Reducibility ($\mathsf{RED}$):
$$\mathsf{(\forall x_1, \ldots, x_n \in W) ((\exists y) \phi \to (\exists y \in W) \phi)}$$
where $\mathsf{\phi}$ is a formula in $\mathsf{L(\in)}$ whose free variables are among $\mathsf{x_1, \ldots, x_n, y}$.
Extensionality ($\mathsf{EXT}$):
$$\mathsf{(\forall z) (z \in x \leftrightarrow z \in y) \to (\forall z) (x \in z \leftrightarrow y \in z)}$$
That is, sets that contain the same elements are contained in the same sets.

Let $\mathsf{S = SS + RED}$. Let $\mathsf{K(W) = S + EXT}$.
Theorem 1: $\mathsf{S}$ interprets $\mathsf{ZFC}$.
Theorem 2: $\mathsf{K(W)}$ proves all of $\mathsf{ZFC}$ except for Foundation and Choice.
Theorem 3: Every theorem of $\mathsf{K(W)}$ that doesn't mention $\mathsf{W}$ can be proved in $\mathsf{ZFC}$ without Foundation and Choice.
Paper 2 also has simple 2-schema system that "goes far beyond even ZFC, and into the depths of the mysterious large cardinal hierarchy. Roughly at the level of strong forms of
indescribable cardinals."


*

*Harvey M. Friedman. Axiomatization of set theory by extensionality, separation, and reducibility: seminar notes. 1997 October 5.


*Harvey M. Friedman. From Russell's paradox to higher set theory. 1997 October 10.


*Harvey M. Friedman. The interpretation of set theory in mathematical predication theory: preliminary report. 1997 October 25.
