nLab metalanguage





The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

homotopy levels




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

ϕtrue \vdash \phi \, true

and then called a judgement instead (in type theory one might also omit the “truetrue”, 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

ψtrueϕtrue \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

ψtrueϕtrue \psi \, true \vdash \phi \, true

holds in the metalanguage, then the judgement

(ψϕ)true \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.)



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.