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
metainformation « Meta-IV « METAL « metalanguage
» Metal Oxide Semiconductor » Metal Oxide
Semiconductor Field Effect Transistor » metaphone