Axiomatic system

As an example, observe the following axiomatic system, based on first-order logic with additional semantics of the following countably infinitely many axioms added (these can be easily formalized as an axiom schema):

${\displaystyle \exists x_{1}:\exists x_{2}:\lnot (x_{1}=x_{2})}$ (informally, there exist two different items).

${\displaystyle \exists x_{1}:\exists x_{2}:\exists x_{3}:\lnot (x_{1}=x_{2})\land \lnot (x_{1}=x_{3})\land \lnot (x_{2}=x_{3})}$ (informally, there exist three different items).

${\displaystyle ...}$

Informally, this infinite set of axioms states that there are infinitely many different items. However, the concept of an infinite set cannot be defined within the system — let alone the cardinality of such as set.

The system has at least two different models – one is the natural numbers (isomorphic to any other countably infinite set), and another is the real numbers (isomorphic to any other set with the cardinality of the continuum). In fact, it has an infinite number of models, one for each cardinality of an infinite set. However, the property distinguishing these models is their cardinality — a property which cannot be defined within the system. Thus the system is not categorial. However it can be shown to be complete.

Mathematical methods developed to some degree of sophistication in ancient Egypt, Babylon, India, and China, apparently without employing the axiomatic method.

Euclid of Alexandria authored the earliest extant axiomatic presentation of Euclidean geometry and number theory. Many axiomatic systems were developed in the nineteenth century, including non-Euclidean geometry, the foundations of real analysis, Cantor's set theory, Frege's work on foundations, and Hilbert's 'new' use of axiomatic method as a research tool. For example, group theory was first put on an axiomatic basis towards the end of that century. Once the axioms were clarified (that inverse elements should be required, for example), the subject could proceed autonomously, without reference to the transformation group origins of those studies.

Not every consistent body of propositions can be captured by a describable collection of axioms. In recursion theory, a collection of axioms is called recursive if a computer program can recognize whether a given proposition in the language is a theorem. Gödel's first incompleteness theorem then tells us that there are certain consistent bodies of propositions with no recursive axiomatization. Typically, the computer can recognize the axioms and logical rules for deriving theorems, and the computer can recognize whether a proof is valid, but to determine whether a proof exists for a statement is only soluble by "waiting" for the proof or disproof to be generated. The result is that one will not know which propositions are theorems and the axiomatic method breaks down. An example of such a body of propositions is the theory of the natural numbers, which is only partially axiomatized by the Peano axioms (described below).

In practice, not every proof is traced back to the axioms. At times, it is not even clear which collection of axioms a proof appeals to. 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.

Any more-or-less arbitrarily chosen system of axioms is the basis of some mathematical theory, but such an arbitrary axiomatic system will not necessarily be free of contradictions, and even if it is, it is not likely to shed light on anything. Philosophers of mathematics sometimes assert that mathematicians choose axioms "arbitrarily", but it is possible that although they may appear arbitrary when viewed only from the point of view of the canons of deductive logic, that appearance is due to a limitation on the purposes that deductive logic serves.

The mathematical system of natural numbers 0, 1, 2, 3, 4, ... is based on an axiomatic system first devised by the mathematician Giuseppe Peano in 1889. He chose the axioms, in the language of a single unary function symbol S (short for "successor"), for the set of natural numbers to be:

• There is a natural number 0.
• Every natural number a has a successor, denoted by Sa.
• There is no natural number whose successor is 0.
• Distinct natural numbers have distinct successors: if a ≠ b, then Sa ≠ Sb.
• If a property is possessed by 0 and also by the successor of every natural number it is possessed by, then it is possessed by all natural numbers ("Induction axiom").

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.