Independence of an axiom system

A property of an axiom system for a given axiomatic theory, defined as follows: Every axiom in the system is independent, i.e. it is not a logical consequence of the set of other axioms of the system. An axiom system possessing this property is said to be independent.

Independence of an axiom in a given axiomatic theory means that the axiom in question may be replaced by its negation without obtaining a contradiction. In other words, an axiom is independent if and only if there is an interpretation of the theory in which the axiom is false, while all the other axioms are true. The construction of such an interpretation is the classical method for proving independence.

When an axiomatic theory is constructed as a formal system, with the relation of logical consequence being formalized as the concept of deducibility, an axiom is considered independent if it cannot be deduced from the other axioms via the derivation rules of the formal system in question. For a broad range of formal systems (viz. first-order theories), independence relative to deducibility is the same as independence relative to logical consequence.

In relation to formal systems, and calculi (cf. Calculus) in general, it is meaningful to speak of independence of derivation rules. A derivation rule is said to be independent if there exists a theorem of the calculus that cannot be deduced without using the rule in question.

Independence of an axiom is not in itself an indispensable property of an axiomatic theory. It only indicates that the body of initial postulates of the theory is not redundant, implying as it were a certain element of technical convenience. Nevertheless, research into the independence of axiom systems and independence proofs contributes to a better understanding of the theory under investigation. It suffices to mention the influence on the development of mathematics of the problem of the independence of Euclid's fifth postulate in the axiom system for geometry.

References

[1]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Addison-Wesley (1964) (Translated from Russian)
[2]	D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1968–1970)
[3]	A.A. Fraenkel, Y. Bar-Hillel, "Foundations of set theory" , North-Holland (1958)

Comments

The examples most common to mathematicians concern the independence of the continuum hypothesis and the axiom of choice from the usual axioms of set theory: K. Gödel showed that from the axioms of set theory one cannot prove the negation of either the continuum hypothesis or the axiom of choice, while P. Cohen proved that the axioms of set theory do not imply either the continuum hypothesis or the axiom of choice.