Axiom schema

The term axiom scheme referred to in mathematical logic a metalinguistic construction procedure for the preparation of the first-stage axiom systems that can not be specified by a finite number of axioms or are to be specified.

Such an axiom system must not be construed as an infinite set. However, it must be decidable whether a given expression is an axiom of the system.

Term

An axiom schema ( plural: axiom schemata ) is described by a recursive definition. The axioms are to be generated in the recursion given by formulas in which (one or more ) occur metalinguistic wildcards (Scheme variables). Since the schema variables in many cases formulas (or on terms, etc. ) may vary, the recursion is in this case often performed on the ( recursive ) structure of the formulas. In practice, the actual recursion is sometimes not quite aptly formulated as intuitive replacement, etc..

A theory which has a finite system of axioms, will finally called axiomatizable. This axiom systems are perceived generally as an elegant, even if sometimes evidence is less elegant in them.

Examples

Well-known axiom schemes are:

• The induction regimen of the first-stage formulation of the Peano axioms, which form a well-known axiom system for arithmetic of natural numbers.
• The replacement scheme of the axiom system ZFC of set theory.

Since neither the replacement scheme of ZFC nor the induction schema of Peano arithmetic can be replaced by a finite number of axioms, both associated theories are not finite axiomatizable.

Substitutability

The first stage also von Neumann - Bernays - Gödel set theory ( NBG ) speaks generally about classes. It must be specified in NBA when talked about a lot and not generally about a class. In ZFC and NBG, the same statements are provable on quantities, nevertheless NBG has but a finite system of axioms. The axiom schemas of ZFC have been to some extent shifted in formulations with suitable classes.

Within the predicate second order logic axiom schemes can be eliminated if the variables occurring schema placeholder for (one or more digits) are essential relations. The predicate logic allows quantification over higher- level relations. However, ( set of Lindström ) are in a higher -order logic stage, which is more expressive than the first-order predicate logic, neither the compactness theorem nor the Löwenheim - Skolem.