Axiom scheme

from Wikipedia, the free encyclopedia

In mathematical logic, the term axiom scheme denotes a metalinguistic construction rule for the representation of first-level axiom systems that cannot or should not be specified by a finite number of axioms .

Such a system of axioms need not be conceived as an infinite set . But it must be possible to decide whether a given expression is an axiom of the system.


An axiom scheme (plural: axiom schemes) is described by a recursive definition . The axioms to be generated are given in the recursion rule by formulas in which (one or more) metalinguistic placeholders (schema variables) occur. Since the schema variables vary in many cases via formulas (or via terms, etc.), the recursion is often carried out via the (recursive) structure of the formulas. In practice, the actual recursion is sometimes not quite appropriately formulated as an intuitive replacement, etc.

A theory that has a finite system of axioms is called finitely axiomatizable . These axiom systems are usually perceived as more elegant, even if the evidence in them is sometimes less elegant.


Well-known axiom schemes are:

Since neither the substitution scheme of ZFC nor the induction scheme of Peano arithmetic can be replaced by a finite number of axioms, both of the associated theories cannot be finitely axiomatized.


The Von-Neumann-Bernays-Gödel set theory (NBG), which is also first -level , generally speaks about classes . It must be stated in NBG when talking about a quantity and not generally about a class. In ZFC and NBG the same statements can be proven over sets, but NBG has a finite system of axioms. The axiom schemes of ZFC have to a certain extent been shifted into formulations with suitable classes.

Within the second-level predicate logic , axiom schemes can be eliminated if the schema variables that occur are essentially placeholders for (single or multi-digit) relations . The higher level predicate logic allows quantification via relations. However, in a predicate logic of a higher level, which is more expressive than the predicate logic of the first level , the compactness theorem and the Löwenheim-Skolem theorem do not apply ( Lindström theorem ) at the same time .