metalanguage

basic constructions:

strong axioms

further

**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**

logic | category theory | type theory |
---|---|---|

true | terminal object/(-2)-truncated object | h-level 0-type/unit type |

proposition(-1)-truncated objecth-proposition, mere proposition

proofgeneralized elementprogram

cut rulecomposition of classifying morphisms / pullback of display mapssubstitution

cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction

introduction rule for implicationunit for hom-tensor adjunctioneta conversion

logical conjunctionproductproduct type

disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)

implicationinternal homfunction type

negationinternal hom into initial objectfunction type into empty type

universal quantificationdependent productdependent product type

existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalencepath space objectidentity type

equivalence classquotientquotient type

inductioncolimitinductive type, W-type, M-type

higher inductionhigher colimithigher inductive type

completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set

setinternal 0-groupoidBishop set/setoid

universeobject classifiertype of types

modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation

proof netstring diagramquantum circuit

(absence of) contraction rule(absence of) diagonalno-cloning theorem

synthetic mathematicsdomain specific embedded programming language

</table>

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

$\vdash \phi \, true$

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

$\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 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

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

holds in the metalanguage, then the judgement

$\vdash (\psi \to \phi) \, true$

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

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

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)

Last revised on February 24, 2014 at 12:32:06. See the history of this page for a list of all contributions to it.