View source for Axiom scheme

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" />.

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" />.

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>

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.

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====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,   "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  A. Church,   "Introduction to mathematical logic" , '''1''' , Princeton Univ. Press  (1956)</TD></TR></table>