Propositional calculus, first-order logic, and other theories in mathematical logic are defined by their axioms (or axiom schemata, plural: axiom schemata) and inference rules. An axiom schema is a sentential formula representing infinitely many axioms. These axioms are obtained by replacing variables in the schema by any formula. For example, the axiom schema
 | (1) |
in propositional calculus represents the axioms
 | (2) |
 | (3) |
and so on.
It is typical to define a theory by axiom schemata rather than axioms. If axioms but not their schemata are utilized, then substitution for variables should be incorporated into inference rules.
