nLab interpretation

Contents

Context

Model theory

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

semantics

Contents

Idea

In formal logic and model theory, interpretation refers to equipping the syntax of some theory with a semantics. Naïvely this means finding a model (in the category of sets) for the theory. This is subsumed by treating interpretations as functors out of syntactic categories.

Definition

In the language of categorical logic, interpretations are representations of theories inside some category C\mathbf{C}. Depending on the kind of theory (cartesian, regular, coherent, first-order, geometric), an interpretation of TT in C\mathbf{C} is just a (cartesian, regular, coherent, first-order, geometric) functor to C\mathbf{C}.

When C\mathbf{C} is Set, TT is first-order, and the functor (say MM) is logical (in the sense of Makkai-Reyes, equivalently coherent if we take the Morleyization of TT), we get models in the sense usually studied in model theory.

Interpretations of theories in each other

Let T 1T_1 and T 2T_2 be (cartesian, regular, coherent, first-order, geometric) theories. A (cartesian, regular, coherent, first-order, geometric) interpretation T 1T 2T_1 \to T_2 is just a functor between the syntactic categories Def(T 1)Def(T 2)\mathbf{Def}(T_1) \to \mathbf{Def}(T_2).

Elsewhere, interpretations have been defined as assignments of symbols in the language 1\mathcal{L}_1 of T 1T_1 to definable sets of T 2T_2 satisfying various coherence conditions (usually at least product-preserving) which amount to functoriality.

Note that via the duality between taking syntactic categories and internal logics, a model of TT in Set\mathbf{Set} is just an interpretation of TT in the theory Lang(Set)\mathsf{Lang}(\mathbf{Set}).

Bi-interpretations of theories

We say that T 1T_1 and T 2T_2 are bi-interpretable if there are functors (of appropriate logical strength) Def(T 1)Def(T 2)\mathbf{Def}(T_1) \leftrightarrows \mathbf{Def}(T_2) forming an equivalence of categories. One direction of conceptual completeness is that bi-interpretable theories have equivalent categories of models. This follows from the fact that (cartesian, regular, coherent, first-order, geometric) functors are closed under composition, and that equivalent categories induce equivalences of functor categories.

Many notions from geometric stability theory and classification theory? are invariant under bi-interpretability, e.g. stability, quantifier elimination, elimination of imaginaries, etc.

Since bi-interpretations induce equivalences of categories of models, monsters of bi-interpretable first-order theories T 1,T 2T_1, T_2 will have isomorphic automorphism groups, with the isomorphism induced by restrictions along reducts. This indicates the bi-interpretation extends to the imaginaries of T 1T_1 and T 2T_2 also, so that T 1 eqT 2 eqT_1^{\operatorname{eq}} \simeq T_2^{\operatorname{eq}}, in fact uniquely—which is the universal property of the pretopos completion.

Interpretations of models in each other

This notion has appeared in the model-theoretic literature, and is what some model theorists mean when they say “interpretation.” Specialize to first-order logic and models in Set, and fix models M 1T 1,M 2T 2M_1 \models T_1, M_2 \models T_2. An interpretation of M 1M_1 in M 2M_2 is a surjection UfM 1U \overset{f}{\twoheadrightarrow} M_1 for UU some subset of M 2 kM_2^k, some kk \in \mathbb{N}, such that the pullback of f *Xf^*X of any definable (with parameters) set XX of M 1M_1 along ff is again definable in YY. This is enough to induce a logical functor Def(T 1)Def(T 2)\mathbf{Def}(T_1) \to \mathbf{Def}(T_2) (surjectivity implies witnessed existentials continue to be witnessed, and the functor being induced by pullback implies logicalness), in fact a logical functor Def(T 1(M 1))Def(T 2(M 2))\mathbf{Def}(T_1(M_1)) \to \mathbf{Def}(T_2(M_2)) of T 1T_1 and T 2T_2 enriched with the elementary diagrams of M 1M_1 and M 2M_2.

Facts:

  • Every interpretation between theories can be realized as being induced by a concrete interpretation between sufficiently saturated models of those theories.

  • Given an f:UM 1f : U \twoheadrightarrow M_1, any other g:UM 1g : U \twoheadrightarrow M_1 which is also an interpretation M 1M 2M_1 \to M_2 is of the form σf\sigma \circ f for some σAut(M 1)\sigma \in \operatorname{Aut}(M_1).

Examples

  • The construction of the Grothendieck group of a commutative monoid implements a canonical interpretation of the ring \mathbb{Z} in the semiring \mathbb{N} (in fact inside \mathbb{N} viewed as the standard model of Peano arithmetic).

  • The complex field \mathbb{C} is canonically interpreted in the real field \mathbb{R} by identifying \mathbb{C} with 2\mathbb{R}^2 and noting that the multiplication of complex numbers is definable from multiplication on the reals.

Classifying toposes

An interpretation TTT \to T' is precisely the inverse image part of a geometric morphism of classifying toposes (T)(T)\mathcal{E}(T') \to \mathcal{E}(T). In particular, models of TT are points of Set in (T)\mathcal{E}(T).

References

  • wikipedia interpretation (model theory)

  • Wilfrid Hodges, A shorter model theory, Cambridge Univ. Press 1997

  • Olivia Caramello, Topos-theoretic preliminaries.

Last revised on July 29, 2023 at 01:26:59. See the history of this page for a list of all contributions to it.