Hello all, one may look for "minimal system of axioms" for ZFC (or any other theory) in the following (unusual) sense : say that a subset S of ZFC is "sufficient" if there is an explicit procedure that constructs a model of ZFC from any model of S.
Thus, for example, ZF is sufficient since inside ZF we can construct Godel's universe L which is a model for ZFC. My questions : are minimal sufficient subsets of ZFC known? Is extensionality+infinity+(power set)+(separation scheme) sufficient?
I think that you haven't quite asked the question you intended to ask, since $L$ is not a set, but rather a proper class, and of course by the incompleteness theorem no subtheory of ZFC, if consistent, can prove that there is a set model of ZFC. So your remarks about ZF having the property you state are not correct.
Rather, it seems that what you want is a minimal or very weak subtheory $S$ of ZFC such that from any model of $S$ we can construct a model of ZFC. This is the nature of your ZF and $L$ example, which shows that $\text{Con}(ZF)\to\text{Con}(ZFC)$. That is, you are asking for a very weak theory $S$ such that $\text{Con}(S)$ implies $\text{Con}(ZFC)$.
Let me note that no particular finite subtheory $S$ of ZFC can have this property. The reason is that for any such particular $S$, it follows by the Reflection theorem that $S$ holds in some large $V_\alpha$, and so ZFC proves $\text{Con}(S)$. If $\text{Con}(S)$ implied $\text{Con}(ZFC)$, then we would have ZFC proving its own consistency, in contradiction to the incompleteness theorem, unless ZFC were inconsistent.
I pondered this question some time ago. As pointed out by Stefan Geschke, infinity and power set are indispensable. Moreover:
The replacement or collection schema is indispensable: $V_{\omega+\omega}$ is a model of all other axioms of ZFC (including separation).
The sum set axiom is indispensable: $H_{\beth_\omega}$ is a model of other axioms of ZFC.
The collection schema (if included in your axiomatization of ZFC) or extensionality is indispensable. One can build a model of other axioms by essentially taking $V_{\omega+\omega}$, and blowing it up to have a lot of automorphisms. Namely, put $M_0=\varnothing$, $M_{\alpha+1}=2\times\mathcal P(M_\alpha)$, and $M_\gamma=\bigcup_{\alpha<\gamma}M_\alpha$ for limit $\gamma$. Then take the model $\langle M,\in^M\rangle$, where $M=M_{\omega+\omega}$, and $\in^M$ is defined as follows: $x\in^M\langle i,y\rangle$ iff $x\in y$. The only nontrivial axiom to check is the replacement schema. It follows from the following property: if $M\models\exists!x\,\phi(x,\vec a)$, where $\vec a\in M_\alpha$, $\alpha<\omega+\omega$, then the unique witness for $x$ also belongs to $M_\alpha$. This in turn holds because there exists an automorphism $f$ of $M$ which is identical on $M_\alpha$, but which moves all elements of $M-M_\alpha$, namely
$f(\langle i,x\rangle)=\begin{cases}\langle i,x\rangle&\text{if }\langle i,x\rangle\in M_\alpha,\\\\ \langle 1-i,x\rangle&\text{otherwise.}\end{cases}$
On the other hand:
Infinity, sum set, power set, extensionality and replacement interpret ZFC. That's just ZF without foundation: it interprets ZF in the well-founded kernel $WF=\bigcup_\alpha V_\alpha$, and ZF interprets ZFC in $L$.
Infinity, sum set, power set, separation (or replacement) and collection interpret ZFC. This requires some work, but here's at least the definition: the domain of interpretation consists of triples $\langle a,e,x\rangle$ such that $e$ is a well-founded extensional binary relation on $a$, and $x\in a$. Equality is interpreted by the relation $\langle a,e,x\rangle =^*\langle a',e',x'\rangle$ defined to hold iff there exists a partial embedding $f$ of the relational structure $\langle a,e\rangle$ to $\langle a',e'\rangle$ with $e$-transitive domain, $e'$-transitive range, and such that $f(x)=x'$. The elementhood predicate is interpreted by $\langle a,e,x\rangle\in^*\langle a',e',x'\rangle$ iff there exists $y\in a'$ such that $\langle y,x'\rangle\in e'$ and $\langle a,e,x\rangle=^*\langle a',e',y\rangle$. One can check that this is an interpretation of all axioms of ZF without foundation, which in turn interprets ZFC by the previous point.
EDIT: I realized that I'm using here a nonstandard definition of $H_\kappa$ which is equivalent to the usual one for regular $\kappa$, but not for singular. The $H_{\beth_\omega}$ above is meant to denote the set of all sets $x$ such that every set in the transitive closure of $\{x\}$ has cardinality (strictly) less than $\beth_\omega$ (but the transitive closure itself can have cardinality $\beth_\omega$).
Just some minor points:
The situation with the Axiom of Regularity (well-foundedness of the $\in$-relation) is similar to the situation with the Axiom of Choice. In any model of ZF without regularity we can build the usual von Neumann hierarchy $V_\alpha$, $\alpha$ an ordinal, by iterating the power set operation, and the union of the $V_\alpha$'s is a model ZF including Regularity.
Depending on the precise formulation, the Replacement Scheme often implies the Separation Scheme.
As you indicate, Infinity is indispensable, since $V_\omega$ is a model of all the other axioms, and even if the background theory is full ZFC (i.e., if we pretend to live in a universe satisfying ZFC), from $V_\omega$ we cannot build a model of ZFC.
I have to confess that I am not sure what you mean by the Abstraction Scheme. Is this
what I would call Separation? Anyhow, given an uncountable regular cardinal $\kappa$ (such as $\aleph_1$),
$H_\kappa$, the collection of all sets whose transitive closure is of size $<\kappa$,
is a model of ZFC without the Power Set Axiom (I am again assuming ZFC as my background theory). It follows that there is no procedure to build a model of ZFC from a model of ZFC without Power Set. So it seems that any minimal subsystem of ZFC would have to include the Power Set Axiom.
Partial conclusion so far: You need infinitely many axioms by Joel's answer, you don't need AC or Regularity, you don't need Separation if your version of Replacement is sufficiently strong, but you do need Infinity and Power Set.
Note the we have used exactly two types of arguments here (except for the obvious "Axiom A implies Axiom B, so we don't need B"): To show that from a model of some subsystem of ZFC we can construct a model of ZFC, just give the construction and why it works (constructible sets, well founded sets). To show that some axiom is necessary, prove the existence of a model of ZFC without the axiom in ZFC, i.e., show that ZFC implies Con(ZFC without the axiom). The Second Incompleteness Theorem then tells you that there is no procedure to construct a model of ZFC from a model of ZFC without the axiom.
I suspect the following isn't what you wanted, but it does fit the wording in the question: "an explicit procedure that constructs a model of ZFC from any model of S." Let S be Peano arithmetic (PA) plus the axiom "ZFC is consistent" (Con(ZFC)). The proof of G"odel's completeness theorem can be formalized in PA. Under the additional hypothesis of Con(ZFC), it produces $\Delta^0_2$ formulas $U(x)$ and $E(x,y)$ that interpret ZFC. (This means that, in PA + Con(ZFC), one has proofs of all the formulas obtained from ZFC axioms by replacing $x\in y$ by $E(x,y)$ and restricting all quantifiers to range only over things that satisfy $U$.) Thus, given any model M of PA + Con(ZFC), one obtains a model M* of ZFC by taking as its underlying set the set of elements that satisfy $U$ in M and by taking as its membership relation the set of pairs that satisfy $E$ in M. The formulas $U$ and $E$ could in principle be written out explicitly just by following the usual (Henkin) proof of the completeness theorem (but I do not volunteer to do this explicit writing). So these formulas give an explicit procedure for converting models M of PA + Con(ZFC) into models M* of ZFC.
A few additional comments: (1) There's nothing special about ZFC here. The same works for any arithmetically definable theory T, except that the formulas $U$ and $E$ will not be $\Delta^0_2$ but merely $\Delta^0_2$ in T. (2) In general, the definition of "interpretation" should also require provability of $\exists x\,U(x)$; I left it out because, in the case of ZFC, it follows from the interpretation of the axiom of infinity. (3) I suspect that the intention of the question was not something like this but rather that S should be a set theory and that the given and constructed models should agree as to the membership relation. Nevertheless, given that the question allowed other sorts of examples, it seemed worthwhile to point this one out. Note that, if you merely want S to be a set theory but don't care whether the membership relations agree, then what I wrote above still works with the theory of finite sets (ZF with the axiom of infinity replaced by its negation) in place of PA; the two are essentially equivalent.
EDIT: Oops. I overlooked the earlier part of the question, which said that S should be a subset of ZFC. My S isn't, because it includes Con(ZFC).
Observation: This question has a reverse mathematics flavor in the following sense. By the Compactness Theorem, to prove CON(ZFC), it is sufficient to prove the infinite theory consisting of all statements of the form CON(ZFC*) where ZFC* ranges over all finite conjunctions of ZFC statements. Thus, we would be looking for infinite subcollections of these conjunctions sufficient for proving all of them.
