What is the smallest fragment of ZFC that has the same consistency strength as ZFC?

The question in the title is undoubtedly nonsensical, but I am not sure how to state this question properly. Perhaps some examples will help me explain it.

Thanks to Godel and Cohen, we know that ${\sf AC}$ is independent of ${\sf ZF}$. This means that we can feel free to take ${\sf AC}$ as an axiom, because ${\sf ZF}\nvdash\neg{\sf AC}$, so as long as ${\sf ZF}$ is consistent we know ${\sf ZFC}$ is consistent. In other words, we have reduced the problem of proving ${\sf ZFC}$ is consistent to the same question of the weaker theory ${\sf ZF}$.

My question is trying to find out how far we can take this, since I know there are results suggesting the independence of most of the remaining axioms of ${\sf ZF}$. Here's my thought process: Suppose I want to know that my theory $T=A+B+C$ is consistent. If I know $A+B\nvdash\neg C$, then $T$ is consistent if $A+B$ is. If I also know $A\nvdash\neg B$, then $T$ is consistent if $A$ is. And unless $A$ is some trivial logical falsehood like $x\ne x$, the logical axioms alone cannot prove $\neg A$, so if propositional logic is consistent, then $A$ is. But propositional logic is consistent, because it is decidable and so it can be proven consistent with a few truth tables.

Is there some flaw in my argument above, or is there some subset of ${\sf ZF}$ that can not be reduced because we don't know that, say, the axiom of unions is independent from the others? Where does Godel's incompleteness result show its face here? (I may be making some tacit assumption that is equivalent to working a stronger theory, but I don't see it.)

• I am fairly certain that there is no particular answer to that. Minimality is way way overrated, though. Simplicity is much more important, and the schemata appearing in $\sf ZFC$ (only replacement, if you want to keep it short, is enough) are quite simple.$${}$$ Not to mention that it depends a lot on how your formulation goes. With pairing, without pairing, with separation, without separation, weaker formulation of replacement (which requires separation) or the stronger formulation, etc. etc. – Asaf Karagila May 23 '13 at 6:05
• Also, much before Godel and Cohen, von Neumann and Mostowski (I believe?) showed that the axiom of regularity is independent from the rest of the axioms. I also know that there was some research into dropping extensionality -- but that theory ended up as strictly weaker than $\sf ZF$ itself. Power set is obviously a keeper, too. – Asaf Karagila May 23 '13 at 6:10
• No, you have an infinite list of axioms in the replacement schema. And I don't think you can thin it out and keep the schema recursive. – Asaf Karagila May 23 '13 at 6:14
• For each $n$ we can write a sentence $r_n$ that states that replacement holds for $\Sigma_n$ formulas, and we can think of the schema of replacement as given by this family of statements. Obviously, $r_m$ implies $r_n$ for $m\ge n$, so eliminating these axioms one at a time does not achieve anything. On the other hand, by reflection, any finite list of consequences of $\mathsf{ZFC}$ (in particular, any finite subset of the axioms) is provably consistent. (Cont.) – Andrés E. Caicedo May 23 '13 at 14:18
• (Cont.) This is similar to the situation with $\mathsf{PA}$, where for each $n$ we can state with a single statement $i_n$, that induction holds for $\Sigma_n$ formulas. And just as with $\mathsf{ZFC}$, we have that $\mathsf{PA}$ is reflexive, and can prove the consistency of any finite list of consequences. – Andrés E. Caicedo May 23 '13 at 14:21

I think a flaw in your argument is that you must consider what the assumptions are when proving that a statement is independent of a theory. For a non-subtle example, the statement "there is an inaccessible cardinal" is independent of $\mathsf{ZFC}$ because it fails in $V_\kappa$ where $\kappa$ is the least inaccessible cardinal, and holds if there is in fact an inaccessible cardinal. Nevertheless, the theory "$\mathsf{ZFC} + \text{there is an inaccessible cardinal}$" has higher consistency strength than $\mathsf{ZFC}$ itself. This happened because we were implicitly assuming (or at least I was implicitly assuming) the consistency of an inaccessible cardinal for the independence proof.
One might think that this issue could be avoided by only considering independence results that can be obtained by inner models and forcing, rather than by large cardinals. However, one still needs some assumptions to be sure that these inner models and forcing extensions behave as desired. Although the proofs that, say, $\mathsf{CH}$ and $\mathsf{AC}$ are independent of $\mathsf{ZFC}$ may be fairly robust in this regard, many independence proofs are more sensitive to assumptions. For example, to show that the Axiom of Replacement is independent from the others, inner model and forcing methods are not going to work because to show that replacement holds in $L$ and in forcing extensions $V[G]$, you need to use replacement in $V$.
We can show that replacement is independent from the others if we assume that it is consistent with the others, just like we can show that the existence of an inaccessible cardinal is independent of $\mathsf{ZFC}$ if we assume that it is consistent with $\mathsf{ZFC}$. You may encounter similar situations with other axioms, such as Power Set, and this will limit your ability to pare down the collection of axioms in the way you envision.