Axiom schema

First-order logic

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.

Arithmetic

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.

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.^[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.

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.^[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]