Axiom schema
Encyclopedia
In mathematical logic
, an axiom schema (plural: axiom schemata) generalizes the notion of axiom
.
An axiom schema is a formula
in the language 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. Often, such conditions require that certain variables be free, or that certain variables not appear in the subformula or term.
Given that the number of possible subformulas or terms that can be inserted in place of a schematic variable is countably infinite, an axiom schema stands for a countably infinite set of axioms. This set can usually be defined recursive
ly. A theory that can be axiomatized without schemata is said to be finitely axiomatized. Theories that can be finitely axiomatized are seen as a bit more metamathematically elegant, even if they are less practical for deductive work.
Two very well known instances of axiom schemata are the:
It has been proved (first by Richard Montague
) that these schemata cannot be eliminated. Hence Peano arithmetic and ZFC cannot be finitely axiomatized. This is also the case for quite a few other axiomatic theories in mathematics, philosophy, linguistics, etc.
All theorems of ZFC are also theorems of von Neumann–Bernays–Gödel set theory
, but the latter is, quite surprisingly, finitely axiomatized. The set theory New Foundations
can be finitely axiomatized, but only with some loss of elegance.
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
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.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, an axiom schema (plural: axiom schemata) generalizes the notion of axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
.
An axiom schema is a formula
Well-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
in the language of an axiomatic system
Axiomatic system
In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems...
, in which one or more schematic variables appear. These variables, which are metalinguistic constructs, stand for any term or subformula
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
of the system, which may or may not be required to satisfy certain conditions. Often, such conditions require that certain variables be free, or that certain variables not appear in the subformula or term.
Given that the number of possible subformulas or terms that can be inserted in place of a schematic variable is countably infinite, an axiom schema stands for a countably infinite set of axioms. This set can usually be defined recursive
Recursive
Recursive may refer to:*Recursion, the technique of functions calling themselves*Recursive function, a total computable function*Recursive language, a language which is decidable...
ly. A theory that can be axiomatized without schemata is said to be finitely axiomatized. Theories that can be finitely axiomatized are seen as a bit more metamathematically elegant, even if they are less practical for deductive work.
Two very well known instances of axiom schemata are the:
- InductionMathematical inductionMathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
schema that is part of Peano's axioms for the arithmetic of the natural numberNatural numberIn mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s; - Axiom schema of replacementAxiom schema of replacementIn set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory that asserts that the image of any set under any definable mapping is also a set...
that is part of the standard ZFC axiomatization of set theorySet theorySet theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...
.
It has been proved (first by Richard Montague
Richard Montague
Richard Merett Montague was an American mathematician and philosopher.-Career:At the University of California, Berkeley, Montague earned an B.A. in Philosophy in 1950, an M.A. in Mathematics in 1953, and a Ph.D. in Philosophy 1957, the latter under the direction of the mathematician and logician...
) that these schemata cannot be eliminated. Hence Peano arithmetic and ZFC cannot be finitely axiomatized. This is also the case for quite a few other axiomatic theories in mathematics, philosophy, linguistics, etc.
All theorems of ZFC are also theorems of von Neumann–Bernays–Gödel set theory
Von Neumann–Bernays–Gödel set theory
In the foundations of mathematics, von Neumann–Bernays–Gödel set theory is an axiomatic set theory that is a conservative extension of the canonical axiomatic set theory ZFC. A statement in the language of ZFC is provable in NBG if and only if it is provable in ZFC. The ontology of NBG includes...
, but the latter is, quite surprisingly, finitely axiomatized. The set theory New Foundations
New Foundations
In mathematical logic, New Foundations is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica. Quine first proposed NF in a 1937 article titled "New Foundations for Mathematical Logic"; hence the name...
can be finitely axiomatized, but only with some loss of elegance.
Schematic variables in first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
are usually trivially eliminable in second-order logic
Second-order logic
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
, because a schematic variable is often a placeholder for any property
Property
Property is any physical or intangible entity that is owned by a person or jointly by a group of people or a legal entity like a corporation...
or relation
Relation (mathematics)
In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...
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.