Which axioms of ZFC or PA are known to not be derivable from the others?

Solution 1:

There are several interesting issues here.

The first is that there are different axiomatizations of PA and ZFC.

• If you look at several set theory books you are likely to find several different sets of axioms called "ZFC". Each of these sets is equivalent to each of the other sets, but they have subtly different axioms. In one set, the axiom scheme of comprehension may follow from the axiom scheme of replacement; in another set of axioms it may not. That makes the issue of independence harder to answer in general for ZFC; you have to really look at the particular set of axioms being used.
• PA has two different common axiomatizations. For the rest of this answer I will assume the axiomatization from Kaye's book Models of Peano Arithmetic which is based on the axioms for a discretely ordered semring.

The second issue is that both PA and ZFC (in any of their forms) have an infinite number of axioms, because they both have infinite axiom schemes. Moreover, neither PA nor ZFC is finitely axiomatizable. That means, in particular, that given any finite number of axioms of one of these theories, there is some other axiom that is not provable from the given finite set.

Third, just to be pendantic, I should point out that, although PA and ZFC are accepted to be consistent, if they were inconsistent, then every axiom would follow from a minimal inconsistent set of axioms. The practical effect of this is that any proof of independence has to either prove the consistency of the theory at hand, or assume it.

Apart from these considerations, there are other things that can be said, depending on how much you know about PA and ZFC.

In PA, the axiom scheme of induction can be broken into infinitely many infinite sets of axioms in a certain way using the arithmetical hierarchy; these sets of axioms are usually called $\text{I-}\Sigma^0_0$, $\text{I-}\Sigma^0_1$, $\text{I-}\Sigma^0_2$ , $\ldots$. For each $k$, $\text{I-}\Sigma^0_k \subseteq \text{I-}\Sigma^0_{k+1}$. The remaining non-induction axioms of PA are denoted $\text{PA}^-$. Then the theorem is that, for each $k$, there is an axiom in $\text{I-}\Sigma^0_{k+1}$ that is not provable from $\text{PA}^- + \text{I-}\Sigma^0_k$. This is true for both common axiomatizations of PA.

In ZFC, it is usually more interesting to ask which axioms do follow from the others. The axiom of the empty set (for the authors who include it) follows from an instance of the axiom scheme of separation and the fact that $(\exists x)[x \in x \lor x \not \in x]$ is a formula in the language of ZFC that is logically valid in first order logic, so ZFC trivially proves that at least one set exists.

In ZFC, there are some forms of the axiom scheme of separation that follow from the remainder of ZFC when particular forms of the axiom of replacement are used. The axiom of pairing is also redundant from the other axioms in many presentation. There are likely to be other redundancies in ZFC as well, depending on the presentation.

One reason that we do not remove the redundant axioms from ZFC is that it is common in set theory to look at fragments of ZFC in which the axiom of powerset, the axiom scheme of replacement, or both, are removed. So axioms that are redundant when these axioms are included may not be redundant once these axioms are removed.

Solution 2:

This is a community wiki answer to gather references. Please feel free to edit it.

• Abraham Robinson. On the independence of the axioms of definiteness (Axiome der Bestimmtheit), Journal of Symbolic Logic, Volume 4, Number 2 (1939), pp. 69-72.

• Elliott Mendelson, Some Proofs of Independence in Axiomatic Set Theory, Journal of Symbolic Logic, Volume 21, Number 3 (Sep., 1956), pp. 291-303. MR0084463 (18,864c).

• Paul Cohen. The independence of the continuum hypothesis, Proc. Nat. Acad. Sci. U.S.A., Volume 50, Number 6 (1963), pp. 1143–1148. MR0157890 (28 #1118); and The independence of the continuum hypothesis. II, Proc. Nat. Acad. Sci. U.S.A., Volume 51, Number 1 (1964), pp. 105–110. MR0159745 (28 #2962).

• Alexander Abian and Samuel LaMacchia. On the consistency and independence of some set-theoretical axioms. Notre Dame Journal of Formal Logic, Volume 19, Number 1 (1978), pp. 155-158. MR0477290 (81e:04001).

• Greg Oman. On the axiom of union, Arch. Math. Logic, 49 (3), (2010), 283–289. MR2609983 (2011g:03122). See also this MO question, and here. (I do not know of an original reference for the fact that $\mathsf{ZFC}-\mathrm{Union}$ does not suffice to prove the existence of infinite unions. The paper includes the usual proof of this fact, and clarifies precisely which unions can be proved to exist in this theory: $\bigcup x$ exists iff $\{|y|\colon y\in x\}$ is bounded.)