An axiom is independent of a theory , i.e., a collection of sentences, if and only if neither nor its negation is provable from .^[1] Equivalently, and are each consistent with , i.e., some models of make true and others make true. Proving the independence of from is usually done by demonstrating the existence of such models.

If the theory is not itself consistent, then no new axiom is independent, since any sentence is provable in an inconsistent theory. Otherwise, proving independence can be very difficult. Forcing is one commonly used technique, which was developed to prove the independence of the continuum hypothesis from ZFC.^[2]

Showing that an axiom is independent is often helpful for providing a more minimal set of axioms, although many systems, such as ZFC, have axioms which can be derived from other axioms in the system. Such results are also central to the discipline of reverse mathematics, which studies when axioms are necessary (rather than merely sufficient) to prove a theorem.

The Parallel Postulate is the fifth postulate in Euclid's Elements and it is independent from the preceding four postulates. This was first shown by Beltrami who proved the equiconsistency of hyperbolic and Euclidean geometry.^[3] Beltrami's proof makes use of several models of hyperbolic geometry including those now known as the Beltrami–Klein model, the Poincaré disk model, and the Poincaré half-plane model.

The parallel postulate is equivalent to Playfair's axiom that for any given line and point not on , in the plane containing both line and point there is at most one line through that does not intersect , i.e., is parallel to . Euclidean geometry is the geometry which makes all five of Euclid's postulates true, including the parallel postulate. Hyperbolic geometry makes the first four of Euclid's postulates true as well as the axiom that there are at least two distinct lines through that do not intersect . Thus, the consistency of hyperbolic geometry shows that the negation of the parallel postulate is consistent with the other four postulates. There are also other non-Euclidean geometries, such as elliptical geometry and spherical geometry, both of which have no lines through that do not intersect .

The continuum hypothesis (CH) is independent from Zermelo–Fraenkel set theory with Choice (ZFC). CH states there is no set with cardinality between that of the integers and their power set, symbolically, .

Gödel^[4][5] showed that CH cannot be disproved from ZF, even if the axiom of choice (AC) is adopted, i.e. from ZFC. Gödel's proof uses ZF to show that both CH and AC hold in the constructible universe , an inner model of the axioms of ZF. This shows that CH (and AC) are consistent with ZF, assuming that ZF is itself consistent. This kind of relative consistency proof is needed since the consistency of ZF cannot be proved within ZF due to Gödel's incompleteness theorems (but it is widely believed to be true and can be proved in stronger set theories).

Cohen^[6][7] showed that CH cannot be proven from the ZFC axioms, completing the overall independence proof. To prove his result, Cohen developed the method of forcing, which has become a standard tool in set theory. Essentially, this method begins with a model of ZF in which CH holds and constructs another model which contains more sets than the original in a way that CH does not hold in the new model. Cohen was awarded the Fields Medal in 1966 for his proof.

• Axiom independence at PhilPapers