Axiom Schema

An axiom schema is a template that specifies a family of axioms in a formal system. Rather than presenting each axiom separately, it uses placeholders for expressions and states how those placeholders may be replaced. Each permitted replacement produces an instance of the schema. A single template can therefore describe infinitely many axioms. Axiom schemas occur in logic, especially in deductive calculi, formal arithmetic, and axiomatic set theory. They belong to the description of a formal language or theory, rather than necessarily being individual statements within that language. (logic.stanford.edu)

Templates and instances

A schema contains metavariables: symbols standing for expressions rather than for objects in the domain under discussion. For example, in propositional logic,

stands for every formula obtained by replacing $\varphi$ and $\psi$ consistently with propositional formulas. Its instances include

and

Both occurrences of $\varphi$ must receive the same replacement; different metavariables need not receive different formulas. The displayed schema is not a claim about two particular propositions but a specification of the entire family. (logic.stanford.edu)

The distinction is one of logical level. An ordinary variable receives a value when a formula is interpreted; a metavariable receives an expression when a schema is instantiated. A schema must consequently be accompanied by conventions specifying which expressions are admissible and what syntactic restrictions apply. These conventions become particularly important in languages containing quantifiers. (philippschlicht.github.io)

Logical axioms and inference rules

In a Hilbert-style calculus, logical axioms are commonly specified by a few schemas. The example above is a tautological pattern: every propositional instance has logical validity. Other schemas describe the interaction of implication and negation. Together, these schemas and a small collection of rules generate the calculus’s proofs. (logical.stanford.edu)

An axiom schema differs from an inference rule. An axiom instance can be introduced without first deriving premises. A rule permits a conclusion to follow from previously available statements. For example, modus ponens licenses the inference of $\psi$ from $\varphi$ and $\varphi\rightarrow\psi$. A formal proof may therefore contain axiom instances alongside assumptions and results of rule applications. The resulting conclusions are theorems of the system. (logic.stanford.edu)

In first-order logic, schemas involving quantifiers require side conditions. Universal instantiation, for example, permits

only when the term $t$ is free for $x$ in $\varphi$. This condition prevents substitution from accidentally placing a previously free variable under a quantifier, thereby changing the intended meaning. Such restrictions are part of the schema itself. (philippschlicht.github.io)

Induction in arithmetic

The first-order formulation of the Peano axioms includes a schema expressing mathematical induction. For every formula $\varphi(x,\vec y)$ in the language of arithmetic, it includes the universal closure of

Here $Sx$ denotes the successor of $x$, and $\vec y$ represents possible parameters. Each instance asserts that a property holding at zero and preserved by succession holds throughout the domain. (personal.cis.strath.ac.uk)

The schema supplies an induction axiom for every eligible formula, not just for familiar properties of natural numbers. It is an infinite family because formulas can have arbitrarily complicated finite constructions. Nevertheless, a particular proof uses only finitely many instances. The formula placeholder is not a predicate variable quantified within the first-order language. (builds.openlogicproject.org)

Schemas in set theory

Standard presentations of Zermelo–Fraenkel set theory employ schemas of separation and replacement. Separation states that a definable condition selects a subset of any given set:

There is an instance for each suitable formula $\varphi$, with $B$ not free in that formula. The restriction to elements of an existing set is essential: separation does not assert that every condition determines a set without such a bound. (philippschlicht.github.io)

Replacement states that if a formula defines a unique output for every element of a set, the outputs form a set. It concerns definable functional relationships, including those not initially represented by a set-sized function. Each defining formula supplies another instance. These principles are schemas because the ordinary first-order language of set theory quantifies over sets, not directly over all formulas or definable relationships. (people.clas.ufl.edu)

Comparison with second-order axioms

In second-order logic, induction can instead be expressed by one sentence:

Under full second-order semantics, $X$ ranges over every subset of the domain. First-order induction instances concern properties definable by formulas with parameters. The two formulations therefore differ in meaning, not merely in typography. Full second-order induction, together with the other arithmetic axioms, excludes nonstandard elements; first-order Peano arithmetic admits nonstandard models. This distinction is central in model theory. (builds.openlogicproject.org)

Finite descriptions and finite axiomatizations

A finite list of schemas is not necessarily a finite list of axioms. In proof theory, this distinguishes a compact specification from a genuinely finite axiomatization by individual sentences. Likewise, the use of an infinite schema alone does not establish that a theory cannot have another, finite axiomatization: that requires a separate mathematical argument. Regardless of the size of the available axiom family, each ordinary formal proof is finite and draws on only finitely many instances. (philippschlicht.github.io)