Axiom schema

An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables appear.

These variables, which are metalinguistic constructs, stand for any term or subformula of the system, which may or may not be required to satisfy certain conditions.

Two well known instances of axiom schemata are the: Czesław Ryll-Nardzewski proved that Peano arithmetic cannot be finitely axiomatized, and Richard Montague proved that ZFC cannot be finitely axiomatized.

The set theory New Foundations can be finitely axiomatized through the notion of stratification.

Higher-order logic allows quantified variables to range over all possible properties or relations.