In
logic, a metatheorem is a statement about a
formal system proven in a
metalanguage. Unlike theorems proved within a given formal system, a metatheorem is proved within a
metatheory, and may reference concepts that are present in the metatheory but not the object theory.
A formal system is determined by a formal language and a
deductive system (
axioms and
rules of inference). The formal system can be used to prove particular sentences of the formal language with that system. Metatheorems, however, are proved externally to the system in question, in its metatheory. Common metatheories used in logic are
set theory (especially in
model theory) and
primitive recursive arithmetic
Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician , reprinted in translation in as a formalization of his finitist conception of the foundations of ...
(especially in
proof theory). Rather than demonstrating particular sentences to be provable, metatheorems may show that each of a broad class of sentences can be proved, or show that certain sentences cannot be proved.
Examples
Examples of metatheorems include:
* The
deduction theorem for
first-order logic says that a sentence of the form φ→ψ is provable from a set of axioms ''A'' if and only if the sentence ψ is provable from the system whose axioms consist of φ and all the axioms of ''A''.
* The
class existence theorem of
von Neumann–Bernays–Gödel set theory states that for every formula whose
quantifiers range only over sets, there is a
class
Class or The Class may refer to:
Common uses not otherwise categorized
* Class (biology), a taxonomic rank
* Class (knowledge representation), a collection of individuals or objects
* Class (philosophy), an analytical concept used differently ...
consisting of the
set
Set, The Set, SET or SETS may refer to:
Science, technology, and mathematics Mathematics
*Set (mathematics), a collection of elements
*Category of sets, the category whose objects and morphisms are sets and total functions, respectively
Electro ...
s satisfying the formula.
*
Consistency proofs of systems such as
Peano arithmetic.
See also
*
Metamathematics
*
Use–mention distinction
References
*
Geoffrey Hunter (1969), ''Metalogic''.
* Alasdair Urquhart (2002), "Metatheory", ''A companion to philosophical logic'', Dale Jacquette (ed.), p. 307
External links
''Meta-theorem'' at Encyclopaedia of Mathematics*
{{Metalogic
Metalogic
Mathematical terminology