Which, if any, axioms of ZFC are known to not be derivable from the other axioms?
Which, if any, axioms of PA are known to not be derivable from the other axioms?

  • $\begingroup$ Well, the ones often talked about are regularity/foundation, replacement, and choice (even such limited choice principles as the axiom of choice for countable sets of finite sets). Choice and the continuum hypothesis were proven independent by Gödel and Cohen. von Neumann proved foundation consistent; the one most closely associated with negations of foundation is Aczel. The axiom of infinity is occasionally dropped as well. Replacement is the oddball there, in that is has a higher "consistency strength" than the rest. $\endgroup$ – dfeuer Jul 2 '13 at 0:15
  • $\begingroup$ Axiom of Extensionality is independent of Axiom of Replacement, Power-set, union, and choice. (See Theorem 2 of this article.) (I found this article from an old post in Stackexchange Math) $\endgroup$ – Hanul Jeon Jul 2 '13 at 0:30
  • $\begingroup$ $\forall x(S(x) \neq 0)$ is independent of the other axioms of PA. There are models of arithmetic that satisfy all the axioms of PA except first order induction proving induction is independent. An example is 2x2 matrices with non-negative integer entries. $\endgroup$ – Russell Easterly Jul 2 '13 at 6:51

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.

  • $\begingroup$ I've seen existence derived from separation and infinity, but doesn't ZFC always require a set from which to separate a subset? Where do you propose to stick your formula? $\endgroup$ – dfeuer Jul 2 '13 at 1:08
  • $\begingroup$ @dfeuer: as I alluded in the answer, for any formula $\phi$ (in the language of ZFC), $(\exists x)[\phi \lor \lnot \phi]$ is provable in first-order logic even with no additional axioms. $\endgroup$ – Carl Mummert Jul 2 '13 at 1:11
  • $\begingroup$ You have not explained that at all. $(\exists x)(\top)$ is a form of the axiom of existence! At least, Smullyan and Fitting see it as such. $\endgroup$ – dfeuer Jul 2 '13 at 1:15
  • $\begingroup$ @dfeuer: yes, but it is an axiom of first-order logic alone, so we get it for free. $\endgroup$ – Carl Mummert Jul 2 '13 at 1:17
  • 1
    $\begingroup$ So $\lnot (\forall x) \phi \to (\exists x)\phi$ is also an axiom scheme of ZFC? It's conventional in first-order logic to separate the axioms of an object theory from the logical axioms, which are the same in every theory, and which, in certain derivation systems, do not need to be assumed at all, because they are built into the derivation rules themselves. $\endgroup$ – Carl Mummert Jul 2 '13 at 1:25

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

  • 1
    $\begingroup$ Perhaps we should also indicate what each reference deals with. The 1939 paper by Robinson (third on the list) is on the independence of the axiom of extensionality. $\endgroup$ – Andrés E. Caicedo Jul 2 '13 at 0:57
  • 1
    $\begingroup$ I don't have links off the top of my head, but I think Cohen and Aczel should go on this list. $\endgroup$ – dfeuer Jul 2 '13 at 1:09
  • $\begingroup$ Paul Cohen's paper of course is on the axiom of choice (the continuum hypothesis is shown independent in part 1, choice in part 2). $\endgroup$ – Andrés E. Caicedo Jul 2 '13 at 1:15
  • 1
    $\begingroup$ It may be good to add Gödel on the consistency of the axiom of global choice and of the generalized continuum hypothesis, and von Neumann on the consistency of regularity, although those results lie on the other side. $\endgroup$ – dfeuer Jul 2 '13 at 1:26
  • 1
    $\begingroup$ @dfeuer I don't think we should include every paper on independence, or this will be useless. In particular, I do not see the point of the Felgner-Truss paper being listed here, since BPIT and OE are not part of the standard axiomatization of $\mathsf{ZFC}$. If you think that a similar list for fragments of choice would be useful, we should have it as a different question. $\endgroup$ – Andrés E. Caicedo Jul 2 '13 at 3:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.