Axiom schema

Examples

First-order logic

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

${\displaystyle \mathrm{\forall }x\mathrm{\Phi }(x)\to \mathrm{\Phi }(t)}$

has as instances the formulas obtained by replacing ${\displaystyle \mathrm{\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 \mathrm{\Phi }}$. Rules or axiom schemata of this kind avoid listing separately every formula obtained by the permitted substitutions.

Arithmetic

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

${\displaystyle (\phi (0,\overrightarrow{y})\wedge \mathrm{\forall }x(\phi (x,\overrightarrow{y})\to \phi (Sx,\overrightarrow{y})))\to \mathrm{\forall }x\phi (x,\overrightarrow{y}).}$

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

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

Set theory

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.

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. Hence the replacement and separation schemata cannot simply be eliminated from ZFC by replacing them with finitely many axioms in the same language.

Finite axiomatization

A theory is finitely axiomatizable if there is a finite set of sentences whose deductive closure is exactly the theory. 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.

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.

Finitely axiomatized related theories

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.

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

In higher-order logic

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 \mathrm{\forall }F((F(0)\wedge \mathrm{\forall }x(F(x)\to F(Sx)))\to \mathrm{\forall }xF(x)).}$

In this second-order sentence, ${\displaystyle F}$ is a genuine variable ranging over properties or classes, not a metalinguistic placeholder. 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.

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.