1. [theorem proving] A language in which proofs are manipulated and tactics are programmed, as opposed to the logic itself (the "object language"). The first ML was the metalanguage for the Edinburgh LCF proof assistant.
2. [logic] A language in which to discuss the truth of statements in another language.
in semantics and philosophy, language used for the analysis of object language (language that is used to talk about objects in the world). Thus, a metalanguage may be thought of as a language about another language. Such philosophers as the German-born Logical Positivist Rudolf Carnap and Alfred Tarski, Polish-born mathematician, argued that philosophical problems and philosophical statements can be resolved only when seen in terms of a syntactical framework. The logic of semantics is what determines the truth of a statement, rather than the statement's nonformal, or actual, meaning. Carnap felt that by making use of symbolic notation in a metalanguage and by adhering to rules of logic it was possible to avoid metaphysical judgments, which, in his system, were by definition invalid.