Axiom scheme

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)