basic constructions:
strong axioms
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
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 by a sequent of the form
and then called a judgement instead (in type theory one might also omit the “$true$”, see at propositions-as-types for details on this). Or, more generally, if the truth of $\phi$ depends on the truth of some other proposition $\psi$ then
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 implication expression $(\psi \to \phi)$ may denote another proposition in the object language, a conditional statement. A deduction theorem connects the two, in that it says that if the judgement
holds in the metalanguage, then the judgement
may be deduced; the converse is the rule of modus ponens. (Actually, both the deduction theorem and modus ponens are slightly more general, being relativized to an arbitrary context, but we needn't get into that here.)
Detailed discussion of the difference between judgements in the metalanguage and propositions in the object language is in the foundational lectures