Namespaces
Variants
Actions

Difference between revisions of "Axiom scheme"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
 
Line 1: Line 1:
A unified manner of formulating axioms (cf. [[Axiom|Axiom]]) with the same syntactic structure. A specific axiom scheme is usually realized by an expression <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142901.png" /> (which is most often formulated in a language different from that in which the axioms are written), which fixes the syntactic structure of the scheme, and by using rules which make it possible to obtain any axiom of the initial structure starting from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142902.png" />.
+
{{TEX|done}}
 +
A unified manner of formulating axioms (cf. [[Axiom|Axiom]]) with the same syntactic structure. A specific axiom scheme is usually realized by an expression $\mathfrak A$ (which is most often formulated in a language different from that in which the axioms are written), which fixes the syntactic structure of the scheme, and by using rules which make it possible to obtain any axiom of the initial structure starting from $\mathfrak A$.
  
In the context of previously formulated or unambiguously understandable rules for generating axioms using an expression <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142903.png" />, an axiom scheme is usually referred to as the self-expression of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142904.png" />. For instance, one speaks of the axiom scheme <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142905.png" /> of propositional calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142906.png" /> when one means the set of axioms of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142907.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142908.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a0142909.png" /> are arbitrary formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a01429010.png" />.
+
In the context of previously formulated or unambiguously understandable rules for generating axioms using an expression $\mathfrak A$, an axiom scheme is usually referred to as the self-expression of $\mathfrak A$. For instance, one speaks of the axiom scheme $\alpha\supset(\beta\supset\alpha)$ of propositional calculus $P$ when one means the set of axioms of the form $A\supset(B\supset A)$, where $A$ and $B$ are arbitrary formulas in $P$.
  
 
An example of a scheme of non-logical axioms is the following variant of the induction scheme in the traditional axiomatizations of arithmetic:
 
An example of a scheme of non-logical axioms is the following variant of the induction scheme in the traditional axiomatizations of arithmetic:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a01429011.png" /></td> </tr></table>
+
$$(\alpha(0)\&\forall x(\alpha(x)\supset\alpha(x')))\supset\forall x\alpha(x),$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a01429012.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014290/a01429013.png" /> are assumed not to belong to the alphabet of the language of the formalization considered and are interpreted, respectively, as an arbitrary formula and an arbitrary variable of this formalization.
+
where $\alpha$ and $x$ are assumed not to belong to the alphabet of the language of the formalization considered and are interpreted, respectively, as an arbitrary formula and an arbitrary variable of this formalization.
  
 
The use of an axiom scheme usually permits one to dispense with the rule of substitution when constructing formal theories. Thus, in any sufficiently strong propositional calculus with two derivation rules — the rule of substitution and the rule of conclusion — it is possible to conduct proofs by substituting into axioms only, which makes it possible to modify the calculus in an equivalent manner by replacing each axiom by the respective axiom scheme, and removing the rule of substitution as a derivation rule.
 
The use of an axiom scheme usually permits one to dispense with the rule of substitution when constructing formal theories. Thus, in any sufficiently strong propositional calculus with two derivation rules — the rule of substitution and the rule of conclusion — it is possible to conduct proofs by substituting into axioms only, which makes it possible to modify the calculus in an equivalent manner by replacing each axiom by the respective axiom scheme, and removing the rule of substitution as a derivation rule.

Latest revision as of 16:00, 5 August 2014

A unified manner of formulating axioms (cf. Axiom) with the same syntactic structure. A specific axiom scheme is usually realized by an expression $\mathfrak A$ (which is most often formulated in a language different from that in which the axioms are written), which fixes the syntactic structure of the scheme, and by using rules which make it possible to obtain any axiom of the initial structure starting from $\mathfrak A$.

In the context of previously formulated or unambiguously understandable rules for generating axioms using an expression $\mathfrak A$, an axiom scheme is usually referred to as the self-expression of $\mathfrak A$. For instance, one speaks of the axiom scheme $\alpha\supset(\beta\supset\alpha)$ of propositional calculus $P$ when one means the set of axioms of the form $A\supset(B\supset A)$, where $A$ and $B$ are arbitrary formulas in $P$.

An example of a scheme of non-logical axioms is the following variant of the induction scheme in the traditional axiomatizations of arithmetic:

$$(\alpha(0)\&\forall x(\alpha(x)\supset\alpha(x')))\supset\forall x\alpha(x),$$

where $\alpha$ and $x$ are assumed not to belong to the alphabet of the language of the formalization considered and are interpreted, respectively, as an arbitrary formula and an arbitrary variable of this formalization.

The use of an axiom scheme usually permits one to dispense with the rule of substitution when constructing formal theories. Thus, in any sufficiently strong propositional calculus with two derivation rules — the rule of substitution and the rule of conclusion — it is possible to conduct proofs by substituting into axioms only, which makes it possible to modify the calculus in an equivalent manner by replacing each axiom by the respective axiom scheme, and removing the rule of substitution as a derivation rule.

References

[1] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2] A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956)
How to Cite This Entry:
Axiom scheme. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Axiom_scheme&oldid=16447
This article was adapted from an original article by F.A. Kabakov (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article