Axiom schema

In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) is a rule or template that specifies a family of axioms. A schema contains placeholders together with side conditions saying how those placeholders may be replaced; each permitted replacement is an instance of the schema.^[1][2] Axiom schemata are commonly used to give finite descriptions of theories whose axioms include infinitely many formulas.^[3]

Let ${\displaystyle L}$ be the object language of a formal theory. An axiom schema is a metalinguistic expression, or schema-template, containing one or more placeholders for expressions of ${\displaystyle L}$, together with side conditions specifying the expressions that may replace the placeholders.^[1][2] The resulting object-language formulas are the instances of the schema and are taken as axioms of the theory.

The placeholders in an axiom schema may stand for terms, formulas, predicates, or relations, depending on the formal system. Side conditions often require that a term be free for a variable in a formula, that a variable occur free in a formula, or that a variable not occur free in a specified formula.^[3] Such conditions are part of the schema, not additional axioms of the object language.

This distinguishes a schematic letter from an ordinary object-language variable. For example, a schematic letter may be a placeholder for any formula of a language, whereas an object-language variable ranges over objects in the domain of interpretation.^[1]

Many Hilbert-style presentations of first-order logic use axiom schemata. For example, the quantifier axiom schema

${\displaystyle \forall x\,\Phi (x)\rightarrow \Phi (t)}$

has as instances the formulas obtained by replacing ${\displaystyle \Phi }$ with an object-language formula and ${\displaystyle t}$ with a term, subject to the condition that ${\displaystyle t}$ is free for ${\displaystyle x}$ in ${\displaystyle \Phi }$.^[3] Rules or axiom schemata of this kind avoid listing separately every formula obtained by the permitted substitutions.

A standard first-order presentation of Peano arithmetic includes the induction schema. For every formula ${\displaystyle \varphi (x,{\vec {y}})}$ in the language of arithmetic, with possible parameters ${\displaystyle {\vec {y}}}$, the schema has an instance of the form

${\displaystyle {\bigl (}\varphi (0,{\vec {y}})\land \forall x(\varphi (x,{\vec {y}})\rightarrow \varphi (Sx,{\vec {y}})){\bigr )}\rightarrow \forall x\,\varphi (x,{\vec {y}}).}$

Thus the induction principle is not a single first-order axiom but a family of axioms, one for each admissible formula ${\displaystyle \varphi }$.^[3][4]

Czesław Ryll-Nardzewski proved that first-order Peano arithmetic is not finitely axiomatizable in its usual language.^[5] Consequently, the induction schema cannot be replaced, in that language, by a finite list of axioms with the same deductive consequences.

The standard first-order axiomatization ZFC contains axiom schemata, including the schema of separation and the schema of replacement. In the replacement schema, each formula that defines a functional relation gives an axiom asserting that the image of any set under that definable function is also a set.^[6][7]

Richard Montague proved a non-finite axiomatizability result for ZF-style set theories; in particular, assuming consistency, ZFC is not finitely axiomatizable in its ordinary first-order language.^[8] Hence the replacement and separation schemata cannot simply be eliminated from ZFC by replacing them with finitely many axioms in the same language.

A theory is finitely axiomatizable if there is a finite set of sentences whose deductive closure is exactly the theory.^[9] An axiom schema may be finitely describable while still specifying infinitely many axioms, since the schema is a metatheoretic recipe for generating instances rather than a finite set of object-language sentences.^[10]

Whether a theory is finitely axiomatizable depends on the language in which the theory is formulated. A theory that is not finitely axiomatizable in one language may have a finitely axiomatized conservative extension in a richer language.

Von Neumann–Bernays–Gödel set theory (NBG) extends the language of set theory by adding classes. NBG is a conservative extension of ZFC for statements about sets, but unlike ZFC it can be finitely axiomatized: its class-existence theorem is obtained from finitely many class-existence axioms rather than from a schema.^[7][11]

New Foundations (NF), introduced by W. V. O. Quine, is usually presented with extensionality and a stratified comprehension schema.^[12] Theodore Hailperin showed in 1944 that this comprehension principle is equivalent to a finite conjunction of instances, giving a finite axiomatization of NF.^[13] Later presentations of NF and related systems may take finite axioms as basic and prove stratified comprehension as a theorem.^[14]

Some axiom schemata in first-order theories can be replaced by single axioms in a higher-order language. For example, the first-order induction schema for arithmetic has a second-order analogue in which a variable quantifies over properties or classes directly:

${\displaystyle \forall F{\bigl (}(F(0)\land \forall x(F(x)\rightarrow F(Sx)))\rightarrow \forall x\,F(x){\bigr )}.}$

In this second-order sentence, ${\displaystyle F}$ is a genuine variable ranging over properties or classes, not a metalinguistic placeholder.^[3] The second-order induction axiom and the first-order induction schema are therefore formally different, and the second-order axiom is stronger under the standard semantics for second-order logic.^[3]

Analogously, some first-order set-theoretic schemata can be represented by quantifying over classes or higher-order objects in an expanded language. This is one reason class theories such as NBG can give finite axiomatizations while remaining conservative over ZFC for set-theoretic sentences.^[7][11]

• Axiom schema of predicative separation
• Axiom schema of replacement
• Axiom schema of specification

• Corcoran, John (2006), "Schemata: The Concept of Schema in the History of Logic" (PDF), Bulletin of Symbolic Logic, 12 (2): 219–240, doi:10.2178/bsl/1146620060, S2CID 6909703
• Corcoran, John (2016). "Schema". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy. ISSN 1095-5054. OCLC 429049174.
• Forster, Thomas (2025). "Quine's New Foundations". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy. ISSN 1095-5054. OCLC 429049174.
• Hailperin, Theodore (1944), "A Set of Axioms for Logic", Journal of Symbolic Logic, 9 (1): 1–19, doi:10.2307/2267307, JSTOR 2267307
• Holmes, M. Randall (1998), Elementary Set Theory with a Universal Set, Cahiers du Centre de Logique, vol. 10, Academia-Bruylant, ISBN 9782872094882
• Mendelson, Elliott (1997), An Introduction to Mathematical Logic (4th ed.), Chapman & Hall, ISBN 0-412-80830-7
• Montague, Richard (1961), "Semantical Closure and Non-Finite Axiomatizability I", Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics, Warsaw, 2–9 September 1959, Państwowe Wydawnictwo Naukowe and Pergamon Press, pp. 45–69
• Potter, Michael (2004), Set Theory and Its Philosophy, Oxford University Press, ISBN 9780199269730
• Ryll-Nardzewski, Czesław (1952), "The Role of the Axiom of Induction in Elementary Arithmetic" (PDF), Fundamenta Mathematicae, 39 (1): 239–263, doi:10.4064/fm-39-1-239-263