# nLab metalanguage

foundations

## Foundational axioms

foundational axiom

# Contents

## 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 $\phi$ may denote a proposition in a deductive system, but the statement “$\phi$ can be proven” is not itself a proposition in the deductive system, but a statement in the metalanguage, often denoted

$\vdash \phi \, true$

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

$\psi \, true \vdash \phi \, true$

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

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

## 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)

Revised on September 28, 2012 06:03:05 by Mike Shulman (192.16.204.218)