Working in ZFC, does there exist a set $\Sigma$ of sentences which axiomatizes ZFC (i.e. every sentence in $\Sigma$ is provable from your favorite axiomatization of ZFC, and vice versa) and is minimal with respect to inclusion (i.e. no proper subset of $\Sigma$ axiomatizes ZFC)?
André Nicolas's comments on What is the minimal axiomatization of a set of structures? seem to suggest the answer is yes, but I could not immediately see how to prove it.
I considered the obvious approach via Zorn's lemma, but it doesn't work. Take the set of all axiomatizations of ZFC, partially ordered by reverse inclusion. It is not the case that every chain has an upper bound. Note that for every formula $\varphi$ and every integer $n$, there is a formula equivalent to $\varphi$ having length at least $n$ (we can pad $\varphi$ by $\land$ing it with a bunch of tautologies). Then let $\Sigma_n$ be ZFC, but deleting all the instances of the Replacement and Comprehension schemas (or whatever infinite schemas appear in your favorite axiomatization) in which the formula $\varphi$ has length less than $n$. By the argument just given, $\Sigma_n$ still axiomatizes ZFC, but any upper bound $\Sigma$ for the chain $\Sigma_1 \supset \Sigma_2 \supset \cdots$ contains no instances of these schemas and in fact is finite, so it cannot axiomatize ZFC at all. Hence this chain has no upper bound.
If the answer is yes, is it true that every theory has a minimal axiomatization?
If the answer is no, does there exist a theory which is not finitely axiomatizable and does have a minimal axiomatization? (Every finitely axiomatizable theory certainly does: fix a finite axiomatization and delete axioms one by one until there is something you can no longer prove.)