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.
[citation needed] A formal system is determined by a formal language and a deductive system (axioms and rules of inference).
Metatheorems, however, are proved externally to the system in question, in its metatheory.
[citation needed] Examples of metatheorems include: