Axiomatic system

In mathematics and logic, an axiomatic system or axiom system is a standard type of deductive logical structure, used also in theoretical computer science. It consists of a set of formal statements known as axioms that are used for the logical deduction of other statements. In mathematics these logical consequences of the axioms may be known as lemmas or theorems. A mathematical theory is an expression used to refer to an axiomatic system and all its derived theorems.

A proof within an axiomatic system is a sequence of deductive steps that establishes a new statement as a consequence of the axioms. By itself, the system of axioms is, intentionally, a syntactic construct: when axioms are expressed in natural language, which is normal in books and technical papers, the nouns are intended as placeholder words. The use of an axiomatic approach is a move away from informal reasoning, in which nouns may carry real-world semantic values, and towards formal proof. In a fully formal setting, a logical system such as predicate calculus must be used in the proofs. The contemporary application of formal axiomatic reasoning differs from traditional methods both in the exclusion of semantic considerations, and in the specification of the system of logic in use.

The axiomatic method in mathematics

The reduction of a body of propositions to a particular collection of axioms underlies mathematical research. This dependence was very prominent, and contentious, in the mathematics of the first half of the twentieth century, a period to which some major landmarks of the axiomatic method belong. The probability axioms of Andrey Kolmogorov, from 1933, are a salient example.^[1] The approach was sometimes attacked at "formalism", because it cut away parts of the working intuitions of mathematicians, and those applying mathematics. In historical context, this alleged formalism is now discussed as deductivism, still a widespread philosophical approach to mathematics.^[2]

Timeline of axiomatic systems to 1900

Major axiomatic systems were developed in the nineteenth century. They included non-Euclidean geometry, Georg Cantor's abstract set theory, and Hilbert's revisionist axioms for Euclidean geometry.

Date	Author	Work	Comments
Fourth century BCE to third century BCE	Euclid of Alexandria	The Elements	Known as the earliest extant axiomatic presentation of Euclidean plane geometry, covering also parts of number theory.^[3]
published 1677	Baruch Spinoza	Ethica, ordine geometrico demonstrata	Just as for Principia philosophiae cartesianae of 1663, Spinoza in his Ethics claimed to be using the "geometric method" of Euclid. A modern view is "the contrast is glaring between the aspiration to prove points by way of deductive argument from self-evident axioms and the obvious source of those points from experience of life and at best some mix of theory and intuition."^[4]
1829	Nikolai Lobachevsky	О началах геометрии ("On the Origin of Geometry")	Lobachevsky's paper is now recognised as the first publication on axiomatic plane geometry developed without the parallel axiom of Euclid, so founding the subject of non-Euclidean geometry.
1879	Gottlob Frege	Begriffschrift	Frege published a formal system for the foundations of mathematics. In modern parlance, it was a second-order logic,^[5] with identity relation. It was expressed in a linear notation for parse trees.
1882/3 to 1890s	Walther von Dyck	Axioms for abstract group theory	Von Dyck is credited with the now-standard group theory axioms.^[6] It is clear from von Dyck's introduction of free groups that he was working with the standard concept of abstract group. It is not, however, evident whether the existence of inverse elements was axiomatic: it would follow from the semantic assumption that groups were permutation groups (permutations being invertible by definition) or geometric transformations with the same property. The discursive style of the period did not labour such points. James Pierpont, one of the American "postulate theorists", did have by 1896 a set of axioms for groups. It is of the modern type, though uniqueness of the identity element (for example) was not assumed.^[7]
1888	Richard Dedekind	construction of the real numbers	When Dedekind introduced his construction of real numbers by Dedekind cuts, axioms for the reals were already mathematical folklore; a subset of those would, later, define ordered field. The further requirement was a theory of mathematical limits^[8]. For example, to capture the idea that the real number line forms a linear continuum means dealing with the historical Zeno's paradoxes; and also clarifying the issue of decimal representations not being unique, so that 0.999...=1, by subjecting it to a mathematical proof. Dedekind's modelling of axioms of the reals put these matters on a firm footing. In practice, the theorems proved using Dedekind cuts that were fundamental results in real analysis could also be proved for other constructions, for example using Cauchy sequences of rational numbers. In other words, they were verifiable axioms, an example being the Archimedean property.
1889	Giuseppe Peano	Arithmetices principia, nova methodo exposita	After some earlier work of others, the Peano axioms provided an axiomatic basis for the arithmetical operations on natural numbers, and mathematical induction, that gained wide acceptance.
1898	Alfred North Whitehead	Treatise on Universal Algebra	Whitehead gave the first axiomatic system for Boolean algebra, as introduced by George Boole in fundamental work on logic and probability.^[9]
1899	David Hilbert	Grundlagen der Geometrie	Presented what are now known as Hilbert's axioms, a revised axiomatization of solid geometry.

Situation at the beginning of the 20th century

David Hilbert "was the first who explicitly adopted the axiomatic method as an investigative framework for the study of the foundations of mathematics".^[10] For Hilbert, a major foundational issue was the logical status of Cantor's set theory. In his list of 23 unsolved problems in mathematics from 1900, Hilbert made the continuum hypothesis the first problem on the list.^[11]

Hilbert's sixth problem asked for "axiomatization of all branches of science, in which mathematics plays an important part". He had in mind at least major areas in mathematical physics and probability.^[12]^[13] Of the effect on science, Giorgio Israel has written:

Founded by mathematician Felix Klein ... the Göttingen School, under the influence of David Hilbert, turned its efforts towards ... set theory, functional analysis, quantum mechanics and mathematical logic. It did so by taking on as its methodical principle the axiomatic method that was to revolutionise the science of [the twentieth century], from the theory of probabilities to theoretical physics.^[14]

Israel comments also on cultural resistance, at least in France and Italy, to this "German model" and its international scope.^[14] The initial International Congress of Mathematicians had heard the views of Henri Poincaré from France on mathematical physics; Hilbert's list was a submission to the second Congress.^[15] The Italian school of algebraic geometry took a different attitude to axiomatic work in theory building and pedagogy.^[16]

Timeline of axiomatic systems from 1901

In the period to 1950, much of pure mathematics received widely-accepted axiomatic foundations. Multiple systems coexisted in axiomatic set theory. Mathematics began to be written in a tighter, less discursive if still informal style.

On the other hand, the approach associated with Hilbert of regarding the axiomatic method as fundamental came under criticism. Part of L. E. J. Brouwer's critique of Hilbert's entire program resulted in an axiomatisation of intuitionistic propositional logic by Arend Heyting.^[17] It allowed constructivism in mathematics to be reconciled with "deductivism", by an exchange of logical calculus, under the title of the Brouwer–Heyting–Kolmogorov interpretation.

Date	Author	Work	Comments
1908 to 1922	Ernst Zermelo and Abraham Fraenkel	Zermelo-Fraenkel set theory	Building on Zermelo set theory from 1908, the Zermelo-Fraenkel (ZF) theory provided an axiomatic basis for set theory with a clarified axiom system (adopting a restriction to first-order logic). With the addition of the axiom of choice, the ZFC theory provided a working foundation for much of classical mathematics..^[18]
1910	Ernst Steinitz	Algebraische Theorie der Körper	Steinitz, under the influence of the introduction by Kurt Hensel of the p-adic numbers, gave an axiomatic theory of the field concept in abstract algebra.^[19]
1911 to 1913	Alfred North Whitehead and Bertrand Russell	Principia Mathematica (3 vols.)	A work devoted to the principle of axiomatic formalization of mathematics, that addressed the set theory paradoxes by an idiosyncratic version of type theory (the ramified theory of types).^[20]
1913	Hermann Weyl	Die Idee der Riemannschen Fläche^[21]	Weyl gave the Riemann surface concept of complex analysis an axiomatic treatment, defining it as a complex manifold of dimension one in terms of neighbourhood systems.^[22]
1914	Felix Hausdorff	Grundzüge der Mengenlehre	The book included axioms for what is now called a Hausdorff topological space, building on Weyl's use of neighbourhoods.^[22]
1915	Maurice Fréchet	abstract measures on measure spaces	The ideas of Lebesgue measure and associated integral, introduced firstly on the real line and Euclidean spaces, were handled axiomatically on set systems.^[23]
1920	Stefan Banach	complete normed vector space	Known now as Banach space, it is the classic setting for functional analysis; initially a real vector space was assumed.^[24]
1921	John Maynard Keynes	A Treatise on Probability	Keynes's work subordinated probability to logic, under the influence of Principia Mathematica. It gave an axiomatic treatment of probability interpretations.
1921	Emmy Noether	Idealtheorie in Ringbereichen^[25]	Noether's paper introduced the ascending chain condition on ideals as an axiom in commutative rings, giving a subclass now called Noetherian rings. It allowed a straightforward inductive proof of Hilbert's basis theorem. It is also considered the beginning of an "epoch" in abstract algebra.^[26]^[27]
1923	Norbert Wiener	Wiener process	Wiener constructed a measure defining a stochastic process model of Brownian motion.^[28]
1932	Oswald Veblen and J. H. C. Whitehead	The Foundations of Differential Geometry (1932)	The work gave the accepted axiomatic definition of differential manifold,^[29] apart from certain issues with separation axioms.
1932	John von Neumann	Mathematische Grundlagen der Quantenmechanik, Dirac–von Neumann axioms	Contribution to the mathematical formulation of quantum mechanics, dating back to a 1927 paper by von Neumann, proposing an axiomatisation of the founding works of quantum mechanics, modelled formally on the notations of Paul Dirac, using abstract Hilbert space methods and unbounded operators.^[30]
1933	Andrey Kolmogorov	probability axioms	Kolmogorv's work subordinated, in effect, mathematical probability to measure theory, while leaving its interpretation open. It built therefore expected values on the Lebesgue integral.^[31]
1945	Samuel Eilenberg and Norman Steenrod	Eilenberg–Steenrod axioms	An axiomatic system for homology theory in algebraic topology, it reflected developments since Noether advocated that homology classes be organised on abstract algebra principles.^[26]
1945–1950	Laurent Schwartz	theory of distributions	Using duality for topological vector spaces of test functions, Schwartz gave a unified axiomatic treatment of the Dirac delta-function and a number of other formal operator methods, and the geometric theory of currents.^[32]

Situation at mid-20th century

Three prominent features of mathematics in 1950 were:

The continuing publication in France by the Bourbaki group of the book series Éléments de mathématique. It aimed at an encyclopedic treatment of foundational concepts.
A dynamic situation in the foundations of algebraic geometry, following the publication of Foundations of Algebraic Geometry by André Weil.
Quantum field theory (QFT), which lacked a satisfactory axiomatic foundation.

Axiomatics à la Bourbaki

The aims of Bourbaki were for a treatment in the large of mathematics, which would be: (a) axiomatic, based down on a stripped-down logical foundation in set theory; (b) in the tradition of Hilbert and the Göttingen School, though excluding the needs of physics and computation; (c) a French reception of current developments. The initial work was carried out in a sharp young Turk reaction against the Cours d'analyse mathématique, a standard text on classical analysis from the beginning of the 20th century, by Édouard Goursat, and in favour of the text Moderne Algebra from the early 1930s on abstract algebra, by Bartel Leendert van der Waerden.^[33]

A pseudonymous paper from 1950, in fact the work of Jean Dieudonné, explained the attitude of Bourbaki to the axiomatic method.^[34]^[35] The principal advantage of working axiomatically is asserted to lie in "elaboration" of mathematical "forms", or structures; this takes precedence over the foundational work and the clarification of inference. What Dieudonné wrote was of his time, as a departure from Hilbert's approaches, and not yet an arrival at structure in the sense implied by the morphisms of category theory.^[35]

Timeline of abstract varieties

For the purposes of the exposition of his proof of the Riemann hypothesis for curves over finite fields, Weil made use of the Jacobian of a curve, and some results of intersection theory. Since he was working over a field of characteristic p rather than the complex numbers, carrying over the classic results required purely algebraic proofs. Further, he used a construction of the Jacobian as an "abstract variety": an intrinsic mathematical object, rather than a projective algebraic variety found in a complex projective space.

A generation later, with the publication of the textbook Algebraic Geometry by Robin Hartshorne, "abstract variety" gained a standard definition within scheme theory.^[36]

Date	Author	Work	Comments
1882	Richard Dedekind and Heinrich Martin Weber	Theorie der algebraischen Functionen einer Veränderlichen	For an irreducible algebraic curve C, defined over the complex numbers, and its function field F, Dedekind and Weber considered a subring R such that F was its field of quotients. The study of ideals in R recovered the points of C, with a finite number of exceptions. The setting was adequate to prove the Riemann-Roch theorem.^[37]
1910	Ernst Steinitz	algebraic closure	Any field K has an algebraic closure, a field that is essentially unique, consisting of all the roots of all the polynomials in one variable having coefficients in K.^[38] The content of the Fundamental Theorem of Algebra amounts to saying that the complex numbers are the algebraic closure of the real numbers. Algebraic geometry over any field K can be conceived of as studying the sets of solutions in its algebraic closure for systems of polynomials in any number of variables.
c.1911–1921	Heinrich Kornblum (1890–1914), Emil Artin	local zeta-functions	After Kornblum's dissertation on a polynomial ring analogue of Dirichlet's theorem on arithmetic progressions used the analogue of non-vanishing of an L-function, Artin's dissertation Quadratische Körper im Gebiete der höheren Kongruenzen on hyperelliptic curve]s over a finite field discussed the generating function now called the local zeta-function of a variety over a finite field.^[39] As a rational function, it had obvious poles; its zeroes became a research topic, as an analogue of the Riemann hypothesis.
1931	Friedrich Karl Schmidt	functional equation for local zeta-function of curves	Weil commented that both Schmidt's work, which applied the Riemann-Roch theorem to prove an analogue of Riemann's functional equation, and Hasse's theorem on elliptic curves, used a straightforward extension of the Dedekind–Weber foundations. It took the algebraic closure of a finite field as field of constants.^[40]
1932	Wolfgang Krull	Allgemeine Bewertungstheorie^[41]	Krull gave axioms for the valuation concept. The set of valuations of the function field of an algebraic variety is related to the birational geometry of the variety; only in the case of curves is the relationship to points of the variety straightforward. The terminology of places, building on valuations, was used by the geometers Oscar Zariski and Shreeram Abhyankar.^[42] Zariski stated that his work was influenced from the 1930s by the Dedekind–Weber paper.^[37]
1941	André Weil	abstract varieties	Weil, at Princeton in spring 1941, in attempting complete foundations for his proof of the Riemann hypothesis for curves over finite fields, required some use of the Jacobian variety over the algebraic closure. He later commented that the algebraists of the school of Emmy Noether were too close to the birational view of the Italian geometers: his need was not met by the birational approach to Jacobians via symmetric products. He used a "piece" of the Jacobian, with its additive structure, as an "abstract" variety. He then found this idea had been implied by Francesco Severi in Trattato di geometria algebrica: pt. 1. Geometria delle serie lineari (1926), pp. 283–4.^[43]
1944	Oscar Zariski	Zariski's abstract Riemann surface (manifold)	The Zariski topology, which for affine space makes the algebraic sets the closed sets, arose around 1941, after a colloquium talk given by Zariski in Princeton.^[44] After some years in which it was mathematical folklore, Zariski published a related result, for valuations. For a field K and subring A, Zariski considered the set of valuation ring in K containing A, and having field of quotients equal to K. These subsets of all such valuation rings in K provided the base of open sets for a topology; and Zariski in geometric cases proved that the space of valuation rings thereby became quasi-compact (i.e. not in general Hausdorff spaces but having the open cover property of compact spaces).^[45]
1942–1944	André Weil	charts for abstract varieties	On his own account, Weil was writing up his Ch. VII of Foundations of Algebraic Geometry, published some years later, under some working assumptions. He adopted the cartographic method, as he called it, as applied by Weyl, Hausdorff, and Veblen and Whitehead; he made no use of the Zariski topology, not yet in print for varieties and associated with birational geometry. He defined intersection number only locally.^[46]
c.1954	Claude Chevalley	schémas (Mark I)	Chevalley came to a foundational concept consisting of a set of local rings, such as the local rings associated with valuations.^[47] He lectured on it in Japan, in 1954.^[48] With the introduction of sheaf theory, it could be considered a ringed space. This definition was transitional.
c.1956	Alexander Grothendieck	scheme theory	A fresh start on axiomatic, abstract foundations for algebraic geometry was made with the definition of a scheme as a ringed space with each point having a neighbourhood of the form Spec(A), where A is a commutative ring and Spec means spectrum of a commutative ring, with points the prime ideals. Grothendieck was working on the theory, for Noetherian rings, in Chevalley's seminar, in 1956. The theory was developed in the book series Éléments de géométrie algébrique, co-authored by Grothendieck and Dieudonné, started in 1958.^[49]

Axiomatic QFT

Plausible axioms for QFT, the Wightman axioms, were introduced by Arthur Wightman. The need for non-trivial examples for these axioms led to constructive quantum field theory, launched by work of Arthur Jaffe and Oscar Lanford, in doctoral dissertations supervised by Wightman in the mid-1960s.^[50]

Axiomatization

In mathematics, axiomatization is the process of taking a body of knowledge and working backwards towards its axioms. It is the formulation of a system of statements (i.e. axioms) that relate a number of primitive terms — in order that a consistent body of propositions may be derived deductively from these statements. Thereafter, the proof of any proposition should be, in principle, traceable back to these axioms.

Axiomatization typically involves choices, and once a theory is axiomatic, it may be possible to change the set of axioms without affecting the mathematical results implied.

Axioms and postulates

In Ancient Greek logic, a contrast between axioms and postulates was recognised ("postulate" being, however, an English term taken from medieval Latin). It reflected, without being applied consistently, axioms as speaking about primitive notions in a way that should be common ground; and postulates as "requests" or "demands", for the purposes of argument. Aristotle's view was minimalist about postulates.^[51]

From the time of Boole's work in the 1840s, in the algebra of logic tradition, logic itself was developed from "postulates" alone. The minimalist view was taken, by the end of the 19th century, to imply research on independence of axioms. Mathematical elegance was also a consideration.^[52] Friedrich Schur criticised the lack of independence of Hilbert's axioms for geometry given in Grundlagen der Geometrie.^[53]

Timeline of postulational analysis

Postulational analysis, according to Susan Stebbing, is what is used "in the construction of a deductive system".^[54] It is a term applied to the correcting or adjusting of axiomatic systems. Axioms may be added to, or removed from, the system; they may be strengthened or weakened. It is also possible to change the logical calculus used for deduction.

Date	Author	Work	Comments
Fourth century BCE to third century BCE	Euclid of Alexandria	The Elements	The Greek term used by Euclid was αἰτήματα (aitēmata).^[51] Its standard English translation is "postulate".^[55]
1882	Moritz Pasch	Pasch's axiom	Pasch introduced an axiom of plane geometry not proved by Euclid, but used by him tacitly.^[56] It was not a consequence of Euclid's axioms, i.e. was independent of Euclid's system.
2024	Terence Tao	Equational Theories Project^[57]	A project to have a complete calibration of theories in equational logic for a magma, where the binary operation is used at most four times. A partial order on the theories makes T≤U when T implies all the theorems implied by U. The purpose of the project was to determine all the cases of ≤, so that an accurate Hasse diagram of the partial order can be drawn. Proof assistant software was used in some cases. The project was completed in April 2025.^[58]

Properties

Four important properties of an axiom system are consistency, relative consistency, completeness and independence. An axiomatic system is said to be consistent if it lacks contradiction. That is, it is impossible to derive both a statement and its negation from the system's axioms.^[59] Consistency is a key requirement for most axiomatic systems, as the presence of contradiction would allow any statement to be proven (principle of explosion). Relative consistency comes into play when we can not prove the consistency of an axiom system. However, in some cases we can show that an axiom system A is consistent if another axiom set B is consistent.^[59]

In an axiomatic system, an axiom is called independent if it cannot be proven or disproven from other axioms in the system. A system is called independent if each of its underlying axioms is independent.^[59] Unlike consistency, in many cases independence is not a necessary requirement for a functioning axiomatic system — though it is usually sought after to minimize the number of axioms in the system.

An axiomatic system is called complete if for every statement, either itself or its negation is derivable from the system's axioms, i.e. every statement can be proven true or false by using the axioms.^[59]^[60] However, note that in some cases it may be undecidable if a statement can be proven or not.

Axioms and models

A model for an axiomatic system is a formal structure, which assigns meaning for the undefined terms presented in the system, in a manner that is correct with the relations defined in the system. If an axiom system has a model, the axioms are said to have been satisfied.^[61] The existence of a model which satisfies an axiom system, proves the consistency of the system.^[62]

Models can also be used to show the independence of an axiom in the system. By constructing a model for a subsystem (without a specific axiom) shows that the omitted axiom is independent if its correctness does not necessarily follow from the subsystem.^[61]

Two models are said to be isomorphic if a one-to-one correspondence can be found between their elements, in a manner that preserves their relationship.^[63] An axiomatic system for which every model is isomorphic to another is called categorical or categorial. However, this term should not be confused with the topic of category theory. The property of categoriality (categoricity) ensures the completeness of a system, however the converse is not true: Completeness does not ensure the categoriality (categoricity) of a system, since two models can differ in properties that cannot be expressed by the semantics of the system.

Incompleteness

If the formal system is not complete not every proof can be traced back to the axioms of the system it belongs. For example, a number-theoretic statement might be expressible in the language of arithmetic (i.e. the language of the Peano axioms) and a proof might be given that appeals to topology or complex analysis. It might not be immediately clear whether another proof can be found that derives itself solely from the Peano axioms.