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.