Axiom scheme
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.
term
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.
Examples
Well-known axiom schemes are:
- The induction scheme of the first-stage formulation of the Peano axioms , which form a well-known system of axioms for the arithmetic of natural numbers .
- The substitution scheme of the axiom system ZFC of set theory .
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.
Substitutability
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 .
literature
- Wolfgang Rautenberg : Introduction to Mathematical Logic . 3. Edition. Vieweg + Teubner , Wiesbaden 2008, ISBN 978-3-8348-0578-2 .
- Wolfgang Rautenberg: measuring and counting . Heldermann Verlag , Lemgo 2007, ISBN 978-3-88538-118-1 , chap. 11: The natural numbers.
- Heinz-Dieter Ebbinghaus , Jörg Flum, Wolfgang Thomas: Introduction to mathematical logic . Springer Spectrum , Berlin 2018, ISBN 978-3-662-58029-5 , chap. 13: Lindström's theorems.