In
logic, a metatheorem is a statement about a
formal system proven in a
metalanguage
In logic and linguistics, a metalanguage is a language used to describe another language, often called the ''object language''. Expressions in a metalanguage are often distinguished from those in the object language by the use of italics, quot ...
. 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
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
(
axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s and
rules of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...
). 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
Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding parts, ...
). 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 In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication ''A'' → ''B'', assume ''A'' as an hypothesis and then proceed to derive ''B''—in systems that do not have an ...
for
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifi ...
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 proof
In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent ...
s of systems such as
Peano arithmetic.
See also
*
Metamathematics
*
Use–mention distinction
The use–mention distinction is a foundational concept of analytic philosophy, according to which it is necessary to make a distinction between a word (or phrase) and it.Devitt and Sterelny (1999) pp. 40–1 W.V. Quine (1940) p. 24 Many philo ...
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