indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
Hrushovski construction?
generic predicate?
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 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.
In the language of categorical logic, interpretations are representations of theories inside some category . Depending on the kind of theory (cartesian, regular, coherent, first-order, geometric), an interpretation of in is just a (cartesian, regular, coherent, first-order, geometric) functor to .
When is Set, is first-order, and the functor (say ) is logical (in the sense of Makkai-Reyes, equivalently coherent if we take the Morleyization of ), we get models in the sense usually studied in model theory.
Let and be (cartesian, regular, coherent, first-order, geometric) theories. A (cartesian, regular, coherent, first-order, geometric) interpretation is just a functor between the syntactic categories .
Elsewhere, interpretations have been defined as assignments of symbols in the language of to definable sets of 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 in is just an interpretation of in the theory .
We say that and are bi-interpretable if there are functors (of appropriate logical strength) 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 will have isomorphic automorphism groups, with the isomorphism induced by restrictions along reducts. This indicates the bi-interpretation extends to the imaginaries of and also, so that , in fact uniquely—which is the universal property of the pretopos completion.
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 . An interpretation of in is a surjection for some subset of , some , such that the pullback of of any definable (with parameters) set of along is again definable in . This is enough to induce a logical functor (surjectivity implies witnessed existentials continue to be witnessed, and the functor being induced by pullback implies logicalness), in fact a logical functor of and enriched with the elementary diagrams of and .
Facts:
Every interpretation between theories can be realized as being induced by a concrete interpretation between sufficiently saturated models of those theories.
Given an , any other which is also an interpretation is of the form for some .
The construction of the Grothendieck group of a commutative monoid implements a canonical interpretation of the ring in the semiring (in fact inside viewed as the standard model of Peano arithmetic).
The complex field is canonically interpreted in the real field by identifying with and noting that the multiplication of complex numbers is definable from multiplication on the reals.
An interpretation is precisely the inverse image part of a geometric morphism of classifying toposes . In particular, models of are points of Set in .
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.