Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’ve expanded Zoran’s entry on type (in model theory), with an ideas section in the language of categorical logic. I’ve also moved definitions to a definition section and briefly mentioned saturation, monster models, and how Barr-exactness of the syntactic category (i.e. elimination of imaginaries) leads to a model-theoretic account of Galois theory—there’s a grey link there which I will flesh out soon.
The work by Awodey and Forssell is related to the work on the topos of types. David posted on category theory and model theory the discussion contains some more links.
Yes, maybe Model theory and the Tannakian formalism by Moshe Kamensky should be mentioned:
The aim of this paper is to exhibit the analogy and relationship between two seemingly unrelated theories. On the one hand, the Tannakian formalism, giving a duality theory between affine group schemes (or, more generally, gerbs) and a certain type of categories with additional structure, the Tannakian categories. On the other hand, a general notion of internality in model theory, valid for an arbitrary first order theory, that gives rise to a definable Galois group. The analogy is made precise by deriving (a weak version of) the fundamental theorem of the Tannakian duality (3.7) using the model theoretic internality.
Also his A categorical approach to internality.
@David_Corfield: I agree! The main construction in that paper is a taking of a sort of internal logic that lands in k-Vect, and later on he briefly sketches how one can modify it to apply to Galois categories rather than tensor categories to get Grothendieck’s Galois theory.
There’s a neat lemma in that second paper I’ve been meaning to find a place for on the nLab for a while: a first-order theory eliminates imaginaries if and only if the ind-completion of its syntactic category is Cartesian-closed; the proof requires Booleanness and compactness in an essential way.
There’s a neat lemma in that second paper I’ve been meaning to find a place for on the nLab for a while: a first-order theory eliminates imaginaries if and only if the ind-completion of its syntactic category is Cartesian-closed; the proof requires Booleanness and compactness in an essential way.
Done: see the new final section of elimination of imaginaries; I’ve also mentioned the -construction and its equivalence with the pretopos completion.
Great you’re doing this! I’m sure the model theoretic pages are in need of considerable development.
It says at type (in model theory):
The simplest first order theories are generalizations of algebraic geometry where points correspond to special (e.g. maximal, prime) ideals in a ring; types generalize points in some of such cases. Other “spectral” intuition also applies.
We should have something on Breiner’s ’Logical schemes’ approach. He uses it among other things to reframe conceptual completeness.
@David: Breiner’s thesis has indeed been on my reading list for a while, though right now I only have a vague picture of how his setup works. There should be a page on the various logical dualities (Makkai’s, Lawvere’s, Awodey-Forssell’s…) and how they relate to the Butz-Moerdijk representaton result. More items on my to-do list!
(Also, the easy direction of conceptual completeness is certainly not “immediate” as he claims in the appendix, though it’s a worthwhile exercise in whiskering :p)
I’ve added a section to elimination of imaginaries on how imaginaries relate to automorphisms (in short, automorphisms of a model have to also act on its interpretation of internal congruences in , so passage to the pretopos completion leaves automorphism groups unchanged). I’ve also spelled out a neat example in this language about “why” has only one nontrivial automorphism.
If as your entry jesse says, you’re just in the first year of a Masters, this is all very impressive.
By the way, you might enjoy this MO question by Jacob Lurie, that I thought some categorical logician might have helped on.
Welcome, jesse!
David 6, the link to Breiner is misformatted. Here is the correct one: Breiner.
jesse 7, I think that saying “logical dualities” is an artifact. Dualities in algebra (e.g. Roos duality, Cartier duality…) and in logic (the ones above and Zawadowski duality etc.) are just instances of the same circle of phenomena and also historically came from the same source. Even superficially you can see the same phenomena like the appearance of ind/pro objects (and the formal topologies equivalent to the consideration of pro-objects in some instances). Historically all came from the generalization of early works of Pontrjagin, Kaplansky, Dieudonne etc. And the dualities in homological algebra and topology (see the paper by Isaksen) like Grothendieck duality are in the same vein as well.
1 to 10 of 10