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”.
]]>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.
]]>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.
]]>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.