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.
1 to 3 of 3
I am quite ignorant of what the impact would be of what you are envisioning above. Conversely my following comment may well be completely useless to you. But since you are posting this question here and hence as an $n$-question, let me say the following anyway:
around here we have been toying around a bit with “modal $\infty$-logics”, namely with the result of starting with homotopy type theory and equipping that with higher modalities (see Mike’s pdf notes), namely with idempotent $\infty$-(co-)monads.
This was driven by a bunch of applications that we ran into, of these idempotent $\infty$-(co-)monads. Specifically we have been playing with two adjoint triples of such which now officially go by the name
shape modality $\dashv$ flat modality $\dashv$ sharp modality
(monad, comonad, monad)
and
reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality
(comonad, monad, comonad)
These modalities turn out to have quite a bit of use in the axiomatization of “geometric” properties in $\infty$-logic. For instance the flat modality characterizes geometrically discrete objects, while the sharp modality characterizes codiscrete object. (The infinitesimal flat modality accordingly characterizes “infinitesimally discrete” objects, namely those that look like de Rham stacks.)
Apart from and in addition to these interpretations, one thing that is interesting here is that these two triples are close to being canonical, in the following sense: among adjoint $n$-tuples of $\infty$-monads, $n = 3$ is somewhat like the largest value for which one can still naturally expect nondegenerate models. Then among adjoint triples, there are exactly the above two choices
$monad \dashv comonad \dashv monad$
$comonad \dashv monad \dashv comonad$.
The only thing on top of just this that I usually add is the requirement that the shape modality also preserves products. (If so, then we call the existence of these modality differential cohesion.) But in applications this appears only every now and then and should probably be regarded as less fundamental than the existence of the two adjoint triples in the first place.
Now, while it has been established that modal homotopy logic with such modalities has plenty of interesting implications and applications, I don’t think anyone so far has looked into this systematically from the point of view of a modal logician. At least David Corfield here has on numerous occasion been pushing in this direction and amplifying the need for further thoughts here, but so far nobody seems to have found the time to follow up on this.
So that would be my spontaneous proposal (me not being a modal logician by a long, long shot, beware): if anyone asks me for suggestions for reasearch a question on modal logic, I would say: explore the modal homotopy type theory induced by adjoint triples of higher modal operators.
At least this question is guaranteed to produce plenty of feedback here on this forum. For whatever that’s worth, of course.
tomr: I worked on $S5_n$ some years ago with an idea of applying it to multi-agent systems (MAS) in AI. There was an interesting problem if you tried to apply the ideas to (abstractions of) actual multiagent systems as used in search engines etc. The problem was that $n$, which was the number of agents involved, was fixed in the modal logic approach, yet in many MAS, agents can be created, say in a search, so as to explore two branches of the search space. In other situations, say with ’agents’ representing sensors sent into some hostile environment, and then it was quite likely that agents would cease to function, so $n$ would change. These sorts of problems suggested some abstract problems as follows.
(i) We have an n-agent system (whose logic is modelled using some sublogic of $S5_n$) and an $m$-agent system (… $S5_m$) and perhaps some communication protocols between them. The $n+m$-agent system that results is some sort of a ’span’ between the the two categories of models of the agents logics. Investigate!!!!
(ii) We have an n-agent system and it is evolving in time, including the possibility of changes to $n$, and to the rules governing the models. How does the category of models of the logic change? Explore some simple cases and see if that suggests some amalgamated models (say involving $S4$ as well since that models time change.)
These problems, and some others, are motivated by practical uses of MAS, but also give purely abstract modal logic problems relating to comparison of different logics and the problems of change within a modal logical system. Those questions are probably too wide to be a detailed source of inspiration for research problems, but if one adds in the sorts of constraint that arise from the use of MAS then the question of the way in which the ’topology’ of the communication between agents provides some guidance as to where to look for problems.
Finally the combinatorial models of $S5_n$ are sets with $n$ equivalence relations. Equivalence relations are groupoids so these are $n$-fold groupoids. Is there any benefit from looking at them in this way? (This begins to be very near to Urs’ questions, as the resulting situation would be to include a reason for the equivalence of two possible worlds in that semantics.) This also relates to models of intuitionistic $S4$ in which path spaces were used. (see work by Eric Goubault and his brother)
1 to 3 of 3