You probably won't like this, but the answer is cardinality 1.
Let C(x) be the statement, "x=0 and the Axiom of Choice holds".
ZF doesn't prove that any x satisifes C(x), since it doesn't prove AC. If AC fails, then no x can have C(x). Thus, ZF+¬AC proves that no x has C(x).
But ZFC proves that C(0) holds, and so it proves that Q={0} is the desired set.
Addendum:
The set { x | C(x) } is an indicator set for AC, in the sense that it is either 0 or 1, depending exactly on whether AC holds. A similar trick works to construct indicator sets for any assertion.
I have suggested that the question be focused on the possibility of projective statements C(x). A projective statement is one expressible in the language of second order number theory, with quantifiers over real numbers and natural numbers. Thus, the question would be whether there is a specific projective statement C(x) such that ZFC proves that Q = { x | C(x) } is nonempty, but ZF does not.
This version of the question is exactly equivalent to the question of whether ZFC is not conservative over ZF for projective sentences, since if there is a counterexample C(X), then the assertion $\exists x C(x)$ is provable in ZFC but not ZF, and if $\sigma$ is provable in ZFC but not in ZF, then the set {x | $\sigma$} is ZFC provably all of the reals, but ZF is consistent with this set being empty.
Therefore, the question amounts to: Is ZFC not conservative over ZF for projective statements?
I think it is not, but I don't have a counterexample.
Meanwhile, I can say that if one replaces ZF here with ZF+DC, looking at the difference between the full Axiom of Choice and the Axiom of Dependent Choices, rather than at the difference between full AC and no AC at all, then the answer is that it IS conservative.
In this MO answer, I explained that ZFC is conservative over ZF+DC for projective sentences, and so if one replaces ZF with ZF+DC in the question, the answer would be no. But without DC, weird things can happen in the reals, and I'm not yet quite sure about it.
I am not sure which statement you heard as the "Ultimate $L$ axiom," but I will assume it is the following version:
There is a proper class of Woodin cardinals, and for all sentences $\varphi$ that hold in $V$, there is a universally Baire set $A\subseteq{\mathbb R}$ such that, letting $\theta=\Theta^{L(A,{\mathbb R})}$, we have that $HOD^{L(A,{\mathbb R})}\cap V_\theta\models\varphi$.
(At least, this is the version of the axiom that was stated during Woodin's plenary talk at the 2010 ICM, which should be accessible from this link. See also the slides for this talk--Thanks to John Stillwell for the link.)
I do not think you will find much about it in the current literature, but Woodin has written a long manuscript ("Suitable extender models") that should probably provide us with the standard reference once it is published.
As stated, this is really an infinite list of axioms (one for each $\varphi$). The statement is very technical, and it may be a bit difficult to see what its connection is with Woodin's program of searching for nice inner models for supercompactness. (That was the topic of his recent series of talks at Luminy; I wrote notes on them and they can be found here.)
Keeping the discussion at an informal level (which makes what follows not entirely correct), what is going on is the following:
Gödel defined $L$, the constructible universe. It is an inner model of set theory, and it can be analyzed in great detail. In a sense (guided by specific technical results), we feel there is only one model $L$, although of course by the incompleteness theorems we cannot expect to prove all its properties within any particular formal framework. Think of the natural numbers for an analogue: Although no formal theory can prove all their properties, most mathematicians would agree that there is only one "true" set of natural numbers (up to isomorphism). This "completeness" of $L$ is a very desirable feature of a model, but we feel $L$ is too far from the actual universe of sets, in that no significant large cardinals can belong to it.
The inner model program attempts to build $L$-like models that allow the presence of large cardinals and therefore are closer to what we could think of as the "true universe of sets"; again, the goal is to build certain canonical inner models that are unique in a sense (similar to the uniqueness of ${\mathbb N}$ or of $L$), and that (if there are "traces" of large cardinals in the universe $V$) contain large cardinals.
The program has been very successful, but progress is slow. One of the key reasons for this slow development is that the models that are obtained very precisely correspond to specific large cardinals, so that, for example, $L[\mu]$, the canonical $L$-like model for one measurable cardinal, does not allow the existence of even two measurable cardinals ($L$ itself does not even allow one).
Currently, the inner model program reaches far beyond a measurable, but far below a supercompact cardinal. Woodin began an approach with the goal of studying the coarse structure of the inner models for supercompactness. This would be the first step towards the construction of the corresponding $L$-like models. (The second step requires the introduction of so-called fine-structural considerations, and it is traditionally significantly more elaborate than the coarse step.)
The results reported in the talks I linked to above indicate that, if the construction of this model is successful, we will actually have built the "ultimate version of $L$", in that the model we would obtain not only accommodates a supercompact cardinal but, in essence, all large cardinals of the universe.
If we succeed in building such a model, then it makes sense to ask how far it is from the actual universe of sets.
A reasonable position (which Woodin seems to be advocating) is that it makes no sense to distinguish between two theories of sets if each one can interpret the other, because then anything that can be accomplished with one can just as well be accomplished with the other, and differences in presentation would just be linguistic rather than mathematical. One could also argue that of two theories, if one interprets the other but not vice versa, then the "richer" one would be preferable. Of course, one would have to argue for reasons why one would consider the richer theory "true" to begin with. This is a multiverse view of set theory (different in details from other multiverse approaches, such as Hamkins's) and rather different from the traditional view of a distinguished true universe.
Our current understanding of set theory gives us great confidence in the large cardinal hierarchy. $\mathsf{ZFC}$ is incomplete, and so is any theory we can describe. However, there seems to be a linear ordering of strengthenings of $\mathsf{ZFC}$, provided by the large cardinal axioms. Moreover, this is not an arbitrary ordering, but in fact most extensions of $\mathsf{ZFC}$ that have been studied are mutually interpretable with an extension of $\mathsf{ZFC}$ by large cardinals (and those for which this is not known are expected to follow the same pattern, our current ignorance being solely a consequence of the present state of the inner model program).
So, for example, we can begin with the $L$-like model for, say, a Woodin cardinal, and obtain from it a model of a certain fragment of determinacy while, beginning with this amount of determinacy, we can proceed to build the inner model for a Woodin cardinal. Semantically, we are explaining how to pass from a model of one theory to a model of the other. But we can also describe the process as establishing the mutual interpretability of both theories. Of course, if we begin with the $L$-like model for two Woodin cardinals, we can still interpret the other theory just as before, but that theory may not be strong enough to recover the model with two Woodin cardinals.
From this point of view, a reasonable "ultimate theory" of the universe of sets would be obtained if we can describe "ultimate $L$" and provide evidence that any extension of $\mathsf{ZFC}$ attainable by the means we can currently foresee would be interpretable from the theory of "ultimate $L$".
The ultimate $L$ list of axioms is designed to accomplish precisely this result.
Part of the point is that we expect $L$-like models to cohere with one another in a certain sense, so we can order them. We, in fact, expect that this order can be traced to the complexity of certain iteration strategies which, ultimately, can be described by sets of reals. Our current understanding suggests that these sets of reals ought to be universally Baire. Finally, we expect that the models of the form $$HOD^{L(A,{\mathbb R})}\cap V_\theta$$ as above, are $L$-like models, and that these are all the models we need to consider. The fact that when $A=\emptyset$ we indeed obtain an $L$-like model in the presence of large cardinals, is a significant result of Steel, and it can be generalized as far as our current techniques allow.
The $\Omega$-conjecture, formulated by Woodin a few years ago, would be ultimately responsible for the $HOD^{L(A,{\mathbb R})}\cap V_\theta$ models being all the $L$-like models we need. (Though I do not quite see that formally the "ultimate $L$" list of axioms supersedes the $\Omega$-conjecture). Also, if there is a nice $L$-like model for a supercompact, then the results mentioned earlier suggest we have coherence for all these Hod-models.
The theory of the universe that "ultimate $L$" provides us with is essentially the theory of a very rich $L$-like model. It will not be a complete theory, by the incompleteness theorems, but any theory $T$ whose consistency we can establish by, say, forcing from large cardinals would be interpretable from it, so "ultimate $L$" is all we need, in a sense, to study $T$. Similarly, only adding large cardinal axioms would give us a stronger theory (but then, this strengthening would be immediately absorbed into the "ultimate $L$" framework).
It is in this sense that Woodin says that the "axiom" would give us a complete picture of the universe of sets. It would also be reasonable to say that this is the "correct" way of going about completing $\mathsf{ZFC}$, since any extension can be interpreted from this one.
[Note I am not advocating for the correctness of Woodin's viewpoint, or saying that it is my own. I feel I do not understand many of the technical issues at the moment to make a strong stance. As others, I am awaiting the release of the "suitable extender models" manuscript. Let me close with the disclaimer that, in case the technical details in what I have mentioned are incorrect, the mistakes are mine.]
Edit: (Jan. 10, 2011) Here is a link to slides of a talk by John Steel. Both Woodin's slides linked to above, and Steel's are for talks at the Workshop on Set Theory and the Philosophy of Mathematics, held at the University of Pennsylvania, Oct. 15-17, 2010. Hugh's talk was on Friday the 15th, John's was on Sunday. John's slides are a very elegant presentation of the motivations and mathematics behind the formulation of Ultimate $L$.
(Jul. 26, 2013) Woodin's paper has appeared, in two parts:
W. Hugh Woodin. Suitable extender models I, J. Math. Log., 10 (1-2), (2010), 101–339. MR2802084 (2012g:03135),
and
W. Hugh Woodin. Suitable extender models II: beyond $\omega$-huge, J. Math. Log., 11 (2), (2011), 115–436. MR2914848.
He is also working on a manuscript covering the beginning of the fine structure theory of these models. I will add a link once it becomes available.
John Steel has a nice set of slides discussing in some detail the multiverse view mentioned above: Gödel's program, CSLI meeting, Stanford, June 1, 2013.
For more on why one may want to accept large cardinals as a standard feature of the universe of sets, see here.
Edit (May 17, 2017): W. Hugh Woodin has written a highly accessible survey describing the current state of knowledge regarding Ultimate $L$. For now, see here (I hope to update more substantially if I find the time):
MR3632568. Woodin, W. Hugh. In search of Ultimate-L. The 19th Midrasha Mathematicae lectures. Bull. Symb. Log. 23 (2017), no. 1, 1–109.
Best Answer
While Kunen takes for universe the collection of all hereditary sets, Marc proposes to restrict the universe to those hereditary sets which are first-order definable without parameters (Marc's "provable sets"). To make this more mathematical, let me rephrase the question as follows:
This turns out to be a delicate question which was answered here on MO some time ago. To summarize the answer there, Marc's proposed universe $K$ will be a model of ZF if and only if $M$ is a model of ZF + V = OD.
Returning to the more philosophical question, this says that Marc's proposal is tenable if and only if there is a reason to believe that the hereditary sets are all ordinal definable. Occam's Razor type arguments support that V = OD and, indeed, V = L is true. However, since it is much weaker than the rigid assumption V = L, the assumption V = OD is not incompatible with a much richer view of the universe...
There is another interpretation of Marc's "provable sets." Instead of merely requiring them to be first-order definable without parameters, one can require them to provably exist in any well-founded model of ZF. With this interpretation, one gets a potentially much smaller set: the minimal well-founded model of ZF. This minimal model is $L_\alpha$ where $\alpha$ is the smallest element of $Ord\cup\{Ord\}$ such that $L_\alpha \models ZF$.
Note that it is entirely plausible that $\alpha = Ord$ (for example this will happen if we happen to live in the minimal model in question). The assumption that "$L_\alpha$ is a set" is equivalent to the existence of a well-founded model of ZF. From a philosophical standpoint, this is a rather strong assertion. For example, it implies that ZF is not only consistent but also $\omega$-consistent and much more...