Definition:Axiom/Formal Systems
Definition
Let $\LL$ be a formal language.
Part of defining a proof system $\mathscr P$ for $\LL$ is to specify its axioms.
An axiom of $\mathscr P$ is a well-formed formula of $\LL$ that $\mathscr P$ approves of by definition.
Axiom Schema
An axiom schema is a well-formed formula $\phi$ of $\LL$, except for it containing one or more variables which are outside $\LL$ itself.
This formula can then be used to represent an infinite number of individual axioms in one statement.
Namely, each of these variables is allowed to take a specified range of values, most commonly WFFs.
Each WFF $\psi$ that results from $\phi$ by a valid choice of values for all the variables is then an axiom of $\mathscr P$.
Also known as
When $\LL$ is a logical language, then one also speaks of logical axioms.
Also see
Sources
- 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 4.2$: The Construction of an Axiom System
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\text{II}.10$ Formal Proofs: Definition $\text{II}.10.1$
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.1$: Definition $3.1$