View source for Axiom schema

{{Short description|Short notation for a set of statements that are taken to be true}}
{{more footnotes|date=May 2016}}
In [[mathematical logic]], an '''axiom schema''' (plural: '''axiom schemata''' or '''axiom schemas''') generalizes the notion of [[axiom]].

==Formal definition==
An axiom schema is a [[well-formed formula|formula]] in the [[metalanguage]] of an [[axiomatic system]], in which one or more [[schematic variable]]s appear. These variables, which are metalinguistic constructs, stand for any [[First-order logic#Formation rules|term]] or [[first-order logic|subformula]] of the system, which may or may not be required to satisfy certain conditions. Often, such conditions require that certain variables be [[free variable|free]], or that certain variables not appear in the subformula or term{{citation needed|date=August 2018}}.

==Examples==
Two well known instances of axiom schemata are the:
* [[mathematical induction|induction]] schema that is part of [[Peano's axioms]] for the arithmetic of the [[natural number]]s;
* [[axiom schema of replacement]] that is part of the standard [[ZFC]] axiomatization of [[set theory]].
[[Czesław Ryll-Nardzewski]] proved that Peano arithmetic cannot be finitely axiomatized, and [[Richard Montague]] proved that ZFC cannot be finitely axiomatized.{{sfn|Ryll-Nardzewski|1952}}{{sfn|Montague|1961}} Hence, the axiom schemata cannot be eliminated from these theories. This is also the case for quite a few other axiomatic theories in mathematics, philosophy, linguistics, etc.

==Finite axiomatization==
Given that the number of possible subformulas or terms that can be inserted in place of a schematic variable is infinite, an axiom schema stands for an infinite [[class (set theory)|class]] or set of axioms. This set can often be [[recursive definition|defined recursively]]. A theory that can be axiomatized without schemata is said to be '''finitely axiomatizable'''.

===Finitely axiomatized theories===
All theorems of [[ZFC]] are also theorems of [[von Neumann–Bernays–Gödel set theory]], but the latter can be finitely axiomatized. The set theory [[New Foundations]] can be finitely axiomatized through the notion of [[stratification (mathematics)|stratification]].

==In higher-order logic==
Schematic variables in [[first-order logic]] are usually trivially eliminable in [[second-order logic]], because a schematic variable is often a placeholder for any [[property]] or [[relation (mathematics)|relation]] over the individuals of the theory. This is the case with the schemata of ''Induction'' and ''Replacement'' mentioned above. Higher-order logic allows quantified variables to range over all possible properties or relations.

==See also==

* [[Axiom schema of predicative separation]]
* [[Axiom schema of replacement]]
* [[Axiom schema of specification]]

==Notes==
{{reflist}}

==References==
* {{Citation|last=Corcoran|first=John|author-link=John Corcoran (logician)|year=2006|title=Schemata: the Concept of Schema in the History of Logic|journal=Bulletin of Symbolic Logic|volume=12|issue=2 |pages=219–240|doi=10.2178/bsl/1146620060 |s2cid=6909703 |url=https://philpapers.org/archive/CORSTC.pdf}}.
* {{Cite SEP |url-id=schema |title=Schema |last=Corcoran |first=John |date=2016}}
* {{Citation |last=Mendelson |first=Elliott |author-link=Elliott Mendelson |year=1997 |title=An Introduction to Mathematical Logic |edition=4th |publisher=Chapman & Hall |isbn=0-412-80830-7}}.
* {{Citation |last = Montague | first = Richard |contribution = Semantic Closure and Non-Finite Axiomatizability I  | editor = Samuel R. Buss | title = Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics | publisher = Pergamon Press | publication-date = 1961 | pages = 45–69}}.
* {{Citation |last=Potter |first=Michael |title=Set Theory and Its Philosophy |publisher=Oxford University Press |year=2004 |isbn=9780199269730}}.
* {{Citation |last=Ryll-Nardzewski |first=Czesław |title=The role of the axiom of induction in elementary arithmetic |url=http://matwbn.icm.edu.pl/ksiazki/fm/fm39/fm39119.pdf |journal=[[Fundamenta Mathematicae]] |volume=39 |pages=239–263 |year=1952|doi=10.4064/fm-39-1-239-263 }}.

{{Set theory}}
{{Mathematical logic}}

[[Category:Formal systems]]
[[Category:Mathematical axioms|*]]