From Wikipedia, the free encyclopedia

In logic, a metatheorem is a true statement about a formal system expressed 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.

Discussion

A formal system is determined by a formal language and a deductive system (i.e. a set of axioms, and a set of deduction rules.) The formal system can thus be used to show that particular sentences of the formal language can be derived from the axioms using the rules.

Metatheorems, on the other hand, are proved externally to the system in question, in another system known as the metatheory. Common metatheories used in logic are set theory (especially in model theory) and primitive recursive arithmetic (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.
• 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

• Barile, Margherita, "Metatheorem" from MathWorld.