Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorPeter Heinig
   • CommentTimeJul 10th 2017
   • (edited Jul 11th 2017)
   • PermaLink
   Author: Peter Heinig
   Format: MarkdownItexIn 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. * **Question:** is there already anything deserving the name `higher model theory' in the sense of a theory giving a Mod-functor which accepts cats inside its argument? Remarks. * *Multidimensional model theory* seems a better term for this field(-to-be). 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, * * what a reasonable multidimensional Mod-functor should be. 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: * * let $\mathbb{A}_{\square}$ denote a specified set containing a specified usual contemporary axiomatization of the concept *monoidal bicategory*, with the middle unitor given by $$ \array{ & & & (o_0\otimes I)\otimes o_1 & \overset{a}{\rightarrow} & o_0\otimes(I\otimes o_1) \\ D_{\square}:= & & & \uparrow & \Downarrow\mu & \downarrow \\ & & & o_0 \otimes o_1 & \overset{\rightarrow}{\mathrm{id}} & o_0\otimes o_1 }$$ * * let $$\array{ & & & (o_0 \otimes I)\otimes o_1 & \overset{a}{\longrightarrow} & o_0 \otimes (I \otimes o_1) & \\ D_{\triangle}:= & & & \searrow & \overset{\mu}{\Rightarrow} & \swarrow & \\ & & & & o_0 \otimes o_1 & & \\ } $$ * * let $\mathbb{A}_{\triangle}:=\mathbb{A}_{\square}\setminus\{D_{\square}\}\cup\{ D_{\triangle}\} $ Note: the set of axioms $\mathbb{A}_{\square}$ appears the more common one nowadays, maybe without any compelling reason. Questions: * * when is $Mod(\mathbb{A}_{\triangle})$ the "same" as $Mod(\mathbb{A}_{\square})$ ? The traditional categorical logic seems not to offer a ready-made answer. What do you consider a usual/reasonable * * * notion of semantics, i.e., how should Mod() be defined here, * * * notion of sameness 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](https://home.sandiego.edu/~shulman/papers/higheril.pdf) provides a useful entry point to relevant modern developments.

   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.

   • Question: is there already anything deserving the name ‘higher model theory’ in the sense of a theory giving a Mod-functor which accepts cats inside its argument?

   Remarks.

   • Multidimensional model theory seems a better term for this field(-to-be).

   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,

   • • what a reasonable multidimensional Mod-functor should be.

   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:

   • • let $\mathbb{A}_{\square}$ denote a specified set containing a specified usual contemporary axiomatization of the concept monoidal bicategory, with the middle unitor given by

   $$\array{ & & & (o_0\otimes I)\otimes o_1 & \overset{a}{\rightarrow} & o_0\otimes(I\otimes o_1) \\ D_{\square}:= & & & \uparrow & \Downarrow\mu & \downarrow \\ & & & o_0 \otimes o_1 & \overset{\rightarrow}{\mathrm{id}} & o_0\otimes o_1 }$$

   • • let

   $$\array{ & & & (o_0 \otimes I)\otimes o_1 & \overset{a}{\longrightarrow} & o_0 \otimes (I \otimes o_1) & \\ D_{\triangle}:= & & & \searrow & \overset{\mu}{\Rightarrow} & \swarrow & \\ & & & & o_0 \otimes o_1 & & \\ }$$

   • • let $\mathbb{A}_{\triangle}:=\mathbb{A}_{\square}\setminus\{D_{\square}\}\cup\{ D_{\triangle}\}$

   Note: the set of axioms $\mathbb{A}_{\square}$ appears the more common one nowadays, maybe without any compelling reason.

   Questions:

   • • when is $Mod(\mathbb{A}_{\triangle})$ the “same” as $Mod(\mathbb{A}_{\square})$ ? The traditional categorical logic seems not to offer a ready-made answer. What do you consider a usual/reasonable
   • • • notion of semantics, i.e., how should Mod() be defined here,
   • • • notion of sameness

   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.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJul 10th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIt sounds like you may be looking for [[2-monads]] and their higher-dimensional generalizations. And, of course, homotopy type theory and its variations is an even more syntactic sort of higher-dimensional syntax.

   It sounds like you may be looking for 2-monads and their higher-dimensional generalizations. And, of course, homotopy type theory and its variations is an even more syntactic sort of higher-dimensional syntax.

3. • CommentRowNumber3.
   • CommentAuthorPeter Heinig
   • CommentTimeJul 12th 2017
   • (edited Jul 12th 2017)
   • PermaLink
   Author: Peter Heinig
   Format: MarkdownItexI realized that, while perhaps more neutral and distinctive, "Multidimensional Model Theory" seems worse than `Higher Model Theory', for a technical reason: to me at least, the bracketing (Multidimensional Model) Theory is always hovering over the proposed phrase, and this is precisely *not* what is mainly meant by it. Multidimensional *models* have, in a sense, be part of traditional model theory since it inception (an example is the model theory of rings---rings have a dimension). The thrust of "Higher Model Theory" is in the direction of multidimensional *syntax*. Phrases like "Multisyntax Model Theory" seem even worse. I will therefore stick with *Higher Model Theory*, which suddenly, by its very vagueness, seems the better term.

   I realized that, while perhaps more neutral and distinctive, “Multidimensional Model Theory” seems worse than ‘Higher Model Theory’, for a technical reason: to me at least, the bracketing

   (Multidimensional Model) Theory

   is always hovering over the proposed phrase, and this is precisely not what is mainly meant by it. Multidimensional models have, in a sense, be part of traditional model theory since it inception (an example is the model theory of rings—rings have a dimension). The thrust of “Higher Model Theory” is in the direction of multidimensional syntax. Phrases like “Multisyntax Model Theory” seem even worse. I will therefore stick with Higher Model Theory, which suddenly, by its very vagueness, seems the better term.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJul 12th 2017
   • (edited Jul 12th 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexWe have recently seen the adjective "higher" as short for "higher homotopy" or "higher categorical" is becoming as popular as it is being misunderstood. And this is misundertanding on top of the clash (which is particularly pronounced for the combination 'higher algebra' ) with traditional use of "higher" as in "higher mathematics". Therefore my suggestion is to keep the "homotopical" or "categorical" in "higher categorical" or "higher homotopical".

   We have recently seen the adjective “higher” as short for “higher homotopy” or “higher categorical” is becoming as popular as it is being misunderstood. And this is misundertanding on top of the clash (which is particularly pronounced for the combination ’higher algebra’ ) with traditional use of “higher” as in “higher mathematics”.

   Therefore my suggestion is to keep the “homotopical” or “categorical” in “higher categorical” or “higher homotopical”.