I was just wondering why there was so little on “Institution independent Model Theory” or Absrtact Model Theory in the wiki. I found this short entry for Abstract Model Theory, and a link to yet non existing page on institutions.
I am trying to use this to see if this can help me extend the semantic Web semantics to modal logic. The reason is that institutions have been used to show the coherence between the different RDF logics - RDFS, OWL, … and so it seems that it should be helpful to go beyond that.
Some papers on semantic web and institutions are listed below. These are great because the semantic web is quite simple, useful, - and I understand it well - and these show in a practical way how to think about institutions, which would be otherwise much more difficult to get into. Also the basics of Abstract Model theory are quite intuitive
The last one ties rdf to Contexts and to Institutions.
The RDF model is actually really simple btw. See the question and answer “What kind of Categorical object is an RDF Model?”
It is nearly self evident from using it that RDF already contains modal logic (see my short example on semweb mailing list), especially as for RDF1.0 xml syntax one can have relations to RDF/XML literals, whose interpretations are of course sets of models, and in RDF1.1 this is made clearer with the notion of DataSets which are sets of graphs. But they have not given a semantics for it… But self evidence does not make for a proof. (and by the way, RDF/XML is really the ugliest syntax existing. Much better to consider N3 which is Tim Berners-Lee’s neat notation for doing logic on the web.
Btw, as an extra part the discussion on modal logic in RDF is tied up with the notion of context, which may just be another way of thinking of modal logic (I am working to see if there is a difference)
So because there was little on the wiki on abstract model theory I was wondering if that was not quite thought of as good Category Theory, or if there just had not been time to complete that page. And for Contexts I was wondering if this was the right place to look at. In the book “Institution independent Model Theory” R Diaconescu has a chapter on Kripke frames, but I think we actually need neighborhood semantics, that is not relations between one world and another but between one world and a set of worlds. So that one can represent inconsistent sets of ideas. (which the web really is a big example of)
]]>In the following,
“cats” is used informally, to have a useful monosyllabic umbrella for ‘anything categorical’
“syntactic” and “semantic” are used informally.
Roughly speaking, the categorical logic developed in the last fifty years connected cats with logic, having cats appear on the semantic side.
Recent developments in mathematics seem to call more and more for technology which routinely handles cats on the syntactic side, too.
In the existent categorical logic, by and large, the “forms” one can handle, in particular—that one can apply the Mod-functor to— remain essentially 1-dimensional things.
Remarks.
More precisely, “multidimensional” seems a better modifier than “higher-dimensional” which in turn seems better than “higher”, for reasons of descriptiveness, neutrality, brevity, etc.
The meaning of the phrase “higher model theory” as it appears in the book edited by Barwise and Feferman is different and one can ignore it (for the purposes of this question, I mean.)
This idea is very much in the air these days, and bits and pieces of it appear all over the place. Just think of all the research on “higher-dimensional syntax” or usages like “a signature is a set of allowed moves” (the latter seems to be used around the Oxford computing lab, having to do with their constructing proof assistants helping to deal with multidimensional syntax). This thread is meant to focus on more technical and localized questions, though, in particular,
Essentially this is the probem of models for higher cats.
To ground the discussion, let me propose an easy test-problem, concerning two “almost equal” sets of multidimensional formulae:
Note: the set of axioms $\mathbb{A}_{\square}$ appears the more common one nowadays, maybe without any compelling reason.
Questions:
for this problem?
Remarks:
I do not expect there to be something essentially new here, but am asking out of curiosity. The possibility of doing apparently trivial modification to a set of formulas of course existed in one-dimensional model theory too, and the usual answer in traditional model theory is that the two sets of models of the two theories so obtained are exactly equal. Still, differences of degree can sometimes turn into something of a difference of kind. There are, intuitively, more possibilities to make seemingly inconsequential changes to a set of diagrammatically-expressed axioms.
The main issue besetting this question seems this: if you opt for some “class of all models” definition of Mod(), together equality of the respective classes, you have to commit to some “ontology” for the models; if on the other hand you opt for some more “constructive”/”algorithmic”/”it’s what you make of it” - definition of Mod(), then the slight difference in the shape of axioms on either side becomes an issue: it will “give the constructor ideas”/”give the algorithm ideas”/”give you ideas”, so that perhaps “what you make of it” comes out different on either side.
Type-theory has probably much to say on the question of how to define Mod, and this lightning overview provides a useful entry point to relevant modern developments.
This is just to suggest another “test problem”, concerning a question implicity asked in the thread
namely how to professionally/routinely/usually handle the fact that according to the usual conventions, one may arbitrarily modify diagrammatically-given axioms by introducing identity arrows into them, and then the resulting diagram, while of course dismissable by “nothing happened, you did the category-theoretic equivalent of a Reidemeister move”, can “trigger” different category-theoretic concepts/ideas: I could point to at least one literature reference which treats the axioms for
by displaying the parallel pair of functors
$\array{ & & & & & \\ & & \overset{cod}{\longrightarrow} & & & \\ \mathsf{D}_1 & & & & & \mathsf{D}_0 \\ & & \overset{dom}{\longrightarrow}& & & \\ & & & & & }$as the span of functors
$\array{ & && & & \\ & & & & & \\ \mathsf{D}_0 & & & \overset{\text{----------------------}}{\text{------------------}} && & \mathsf{D}_0 \\ & \overset{cod}{\nwarrow} & & \overset{dom}{\nearrow} & & \\ & & \mathsf{D}_1 & & & }$which then may “trigger” the concept of pushouts-in-CAT, and another literature reference which arbitrarily”blows-up” the parallel pair of functors into a cospan of functors
$\array{ & && & & \\ & & & & & \\ \mathsf{D}_1 & & & \overset{\text{----------------------}}{\text{------------------}} && & \mathsf{D}_1 \\ & \overset{cod}{\searrow} & & \overset{dom}{\swarrow} & & \\ & & \mathsf{D}_0 & & & }$which may “trigger” the concept of pullbacks-in-CAT.
One of the references actually uses pullbacks-in-CAT in the sequel .
I do not expect there to be much to be said, in particular since pushouts and pullbacks are dual concepts (which in turn is reflected in how small the “edit-distance” from the above code for the above span into the above code of the above cospan is) so that here in a sense even less happens than in the case of the example of monoidal bicategories axiomatized with, alternatively, a triangular or a quadrangular $\mu$iddle unitor. Except for some evident things, such as that a reasonable definition of Mod() should judge
Mod(axiomatization of double-categories with a parallel pair)
“equal” to
Mod(axiomatization of double-categories with a span)
“equal” to
Mod(axiomatization of double-categories with a cospan)
and therefore must somehow always simultaneously be “aware” of both sides of any two dual cat-concepts.
Again, there probably is not much to say here, I am just floating this particularly “trivial” and symmetric and self-dual example. But who knows?
]]>I’ve created the entry Ehrenfeucht-Fraïssé games and recorded the basic definitions and results (partly inspired by jesse’s efforts to add some model theory content to the nlab). I’m running out of steam now, but we should also mention the connections to quantifier elimination and Scott rank. (I’ve added a redirect from back-and-forth argument which was requested at quantifier elimination.)
]]>I have recently created an entry definable set. It is usually defined as an equivalence class of formulas satisfied by the same elements in each structure of the first order language (or model for a theory). But some works recently, like the lectures of David Kazhdan (pdf), take for granted the observation that in fact the relation of equivalence implies that the evaluation of definable sets in a model extends to a functor on the category of models and elementary monomorphismsm, say $\mathcal{M}_{el}$. There are now many other notions in model theory which have ’definable” as a prefix, and they do not fill uniformly in the same pattern. For example, the category of “definable spaces” and “definable continuous maps” is not the same as the functor from $\mathcal{M}_{el}$ to topological spaces and continuous maps, though possibly some examples would probably fit in the latter description. Also some “definable” notions are for a fixed model and not functors on $\mathcal{M}$.
Now, Hrushovski in his 2006 work looked at definable groupoids, about which I just plan to create an entry. Now I was cautious not to say that it is simply an internal groupoid in the category of definable sets, as it is at first defined differently. Besides dealing with internal objects in a large functor category, one should possibly make care about this as well, regarding that we are dealing with a setup where one should be maybe careful about tools like large cardinals (what would be the elegant way to do?).
But in any case, the first problem (that the definition was not given as a functor) can easily be dealt.
So the definition roughly says that one has definable set of objects and of morphisms (just as we wanted), but then the structure maps like target, composition etc. should be definable functions, hence, as relations they are definable subsets of cartesian products, so when presented from $\mathcal{M}_{el}$ as functors into the categories of sets and relations, which are functional in every model. So, now I just checked a very simple fact, specific to the category of sets and functions, that
Proposition. Given a small category $\mathcal{M}$ and two functors $F,G:\mathcal{M}\to Set$ the natural transformations $\alpha : F\to G$ are in 1-1 correspondence with functors $\beta : \mathcal{M}\to Set$ such that $\beta(A) \subset F(A)\times G(A)$ and $\beta(A)$ is a functional relation.
In other words, functoriality of $\beta$ is the same as $\alpha$ being natural. That is new to me.
This immediately implies that the definable groupoid as in Hrushovski arxiv/math.LO/0603413 is (up to the delicacies dealing with functor categories) indeed an internal groupoid in the category of functors $\mathcal{M}_{el}\to Set$ and natural transformations.
]]>sorry, first created it in David Corfields’ web, then in $n$Lab. DId not keep track where I was.
]]>Small A_∞-dg-categories and small dg-categories admit a model structure and the forgetful functor from dg-categories to A_∞-dg-categories is a right Quillen functor so that the resulting Quillen adjunction is actually a Quillen equivalence, which can be seen as a many-objects version of the Quillen equivalence between A_∞-dg-algebras and dg-algebras, as described, for example, by Berger and Moerdijk, “Axiomatic homotopy theory for operads”.
Is there a written source for this Quillen equivalence?
]]>Chevalley’s theorem on constructible sets and elimination of quantifiers. The entries are related ! The interest came partly from teaching some classical algebraic geometry these days. The related entry is also forking, though yet it is not said why; non-forking may be viewed as related to a notion of generic point, generic type (in the sense of model theory).
]]>A stub for metric abstract elementary class. Related changes/additions on some model theory entries like elementary class of structures, forking entered a related blog at math blogs.
]]>Stub for amalgamation.
]]>Finally, definable set.
]]>I have expanded theory adding more basics in classical syntactic approach. I added a new subsection
]]>Set-theoretic models for a first-order theory in syntactic approach
The basic concept is of a structure for a first-order language $L$: a set $M$ together with an interpretation of $L$ in $M$. A theory is specified by a language and a set of sentences in $L$. An $L$-structure $M$ is a model of $T$ if for every sentence $\phi$ in $T$, its interpretation in $M$, $\phi^M$ is true (“$\phi$ holds in $M$”). We say that $T$ is consistent or satisfiable (relative to the universe in which we do model theory) if there exist at least one model for $T$ (in our universe). Two theories, $T_1$, $T_2$ are said to be equivalent if they have the same models.
Given a class $K$ of structures for $L$, there is a theory $Th(K)$ consisting of all sentences in $L$ which hold in every structure from $K$. Two structures $M$ and $N$ are elementary equivalent (sometimes written by equality $M=N$, sometimes said “elementarily equivalent”) if $Th(M)=Th(N)$, i.e. if they satisfy the same sentences in $L$. Any set of sentences which is equivalent to $Th(K)$ is called a set of axioms of $K$. A theory is said to be finitely axiomatizable if there exist a finite set of axioms for $K$.
A theory is said to be complete if it is equivalent to $Th(M)$ for some structure $M$.
Stub for Lascar group, the analogue of Galois group for first order theories.
]]>I’d like to learn about the Jardine-Joyal model structure on simplicial presheaves (and sheaves?) on a site. My understanding is that this was developed in a letter from Joyal to Grothendieck, which is cited pretty widely in the literature. Does anyone have a copy or know where I could find it? (Or, if anyone knows other sources for this model structure, that would also be helpful.)
]]>New stubs Oka principle, Oka manifold (with redirect Oka map) and Franc Forstnerič. Jardine has shown that one can use the Toen-Vezzosi like engineering with his intermediate model structure on the category of simplicial presheaves on a simplicial version of the Stein site. The $(\infty,1)$-stacks/fibrants will be Oka maps; those cofibrants which are represented by complex manifolds are in fact Stein manifolds.
]]>