a theory the subject matter of which is another theory. A finding proved in the former that deals with the latter is known as a metatheorem.

The most notable example of a metatheory was provided by David Hilbert (Hilbert, David), a German mathematician, who in 1905 set out to construct an elementary proof of the consistency of mathematics. For this purpose he needed a theory that studies mathematics and has mathematical proofs as the objects to be investigated. Although theorems proved in 1931 by Kurt Gödel, a Moravian–U.S. mathematical logician, made it unlikely that Hilbert's program could succeed, his metamathematics became the forerunner of much fruitful research. From the late 1920s Rudolf Carnap, a leading philosopher of science and of language, extended this inquiry, under the headings metalogic and logical syntax, to the study of formalized languages in general.

In discussing a formalized language it is usually necessary to employ a second, more powerful language. The former is then known as the object language, whereas the second is its metalanguage.