nLab
metalanguage

Idea

In formal logic, a metalanguage is a language? (formal or informal) in which the symbols and rules for manipulating another (formal) language – the object language – are themselves formulated. That is, the metalanguage is the language used when talking about the object language.

For instance the symbol $\varphi$ may denote a proposition in a deductive system, but the statement “$\varphi$ can be proven” is not itself a proposition in the deductive system, but a statement in the metalanguage, often denoted

$$⊢\varphi \mathrm{true}$$\vdash \phi \, true

and then called a judgement instead. Or, more generally, if the truth of $\varphi$ depends on the truth of some other proposition $\psi$ then

$$\psi \mathrm{true}⊢\varphi \mathrm{true}$$\psi \, true \vdash \phi \, true

is the hypothetical judgement in the metalanguage that there is a proof of $\varphi$ in the context in which $\psi$ is assumed.

In contrast, the expression $(\psi \to \varphi )$ may denote another proposition in the object language, a conditional statement.

Examples

• A system of natural deduction with its type formation/term introduction/term elimination and computation rules is the metalanguage for type theory.

References

Detailed discussion of the difference between judgements in the metalanguage and propositions in the object language is in the foundational lectures

• Per Martin-Löf, On the meaning of logical constants and the justifications of the logical laws, leture series in Siena (1983) (web)