Is there a minimal axiomatization of ZFC?

Question

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.)

Answer 1

Claim: Every countable theory has an independent set of axioms.

Proof: Let $\langle S_n: n < \omega \rangle$ list all theorems of this theory. Inductively construct $\langle T_{k} : k < \omega \rangle$ as follows. Having chosen $T_1, T_2, ..., T_k$, look for least $n$ such that $S_n$ does not follow from $\{T_1, .., T_k\}$. Let $T_{k+1} = (T_1 \wedge T_2 \wedge \dots \wedge T_k) \rightarrow S_n$.

Edit: As Carl Mummert pointed out, it is not clear if one could get a recursive independent set of axioms for every recursively axiomatizable theory. It seems that Kreisel gave an example of a recursively axiomatizable theory with no recursive independent set of axioms. For references see the following FOM post. Finally, ZFC and PA do have recursive independent set of axioms. See here for references. The argument uses the fact that ZFC and PA can prove the consistency of any finite subset of their axioms: If $\{\phi_n : n < \omega\}$ lists their axioms then $\{\psi_n : n < \omega\}$ is an independent axiomatization where $\psi_n = \phi_n \wedge \text{Con}(\psi_1 \wedge \psi_2 \wedge \dots \wedge \psi_{n-1})$.

However, whether the standard systems of axioms for concrete theories like ZFC and PA contains such an independent set of axioms is far from clear.

Answer 2

Here is an algebraic way to visualize a proof (in particular, the proof presented by Minimal in another answer uses this method). Consider the entire Lindenbaum algebra for the language of ZFC, which I arrange so that $\bot$ is the maximal element. I will use AND and OR to represent the logical operators of conjunction and disjunction on formulas.

Then the set of consequences of ZFC is downward closed and upward directed -- if ZFC proves $\phi$ and $\psi$ then it proves $(\phi \operatorname{AND} \psi)$. So the set of consequences of ZFC is an ideal $I_{\text{ZFC}}$ in the algebra. Our goal is simply to prove that this ideal is generated by some antichain in the algebra. We know that ZFC is not finitely axiomatizable, so $I_{\text{ZFC}}$ is not principal, so the antichain will necessarily be infinite if it exists.

Next we verify a standard lemma: for each $\top < B < A$ in this algebra, there is a $C < A$ such that $B$ and $C$ sup to $A$ (so in particular $C \not <B$ and $B\not<C$). One such $C$ is relative complement of $B$ relative to $A$, which is $(\lnot B) \operatorname{OR} A$ (i.e. $B \operatorname{\text{ IMPLIES }} A$).

Given that, let $(\phi_i : I \in \omega)$ be a strictly increasing sequence of of non-$\top$ axioms that generate $I_{\text{ZFC}}$. Let $\psi_1 = \phi_1$. Inductively define $\psi_{i+1}$ such that $\psi_i$ and $\psi_{i+1}$ sup to $\phi_{i+1}$, using the lemma. Then $\{\psi_i : i \in \omega\}$ is the desired axiomatization.

There's nothing special about ZFC here, although you want to treat finitely axiomatizable theories as a special case.

$$ \begin{array}{ccccc} &&&\vdots\\ &&&\phi_3 \\ &&\swarrow & & \searrow\\ &\phi_2 & &&& \psi_3\\ \quad\swarrow & & \searrow\\ \phi_1=\psi_1 & & & \psi_2 \end{array} $$