metalanguage

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.