added pointer to:

- Clarence I. Lewis, Cooper H. Langford, pp 153 & App II of:
*Symbolic Logic*(1932), Dover (2000) [App. II pdf]

also touched and slightly expanded the last paragraphs in the Idea section (the ones on models, starting here)

]]>added (here) a screenshot of the first page from Lemmon & Scott (1977)

(the most satisfactory monograph account I have seen, by a margin)

]]>added pointer to English translation of Becker’s old text:

- Stefania Centrone, Pierluigi Minari,
*Oskar Becker, On the Logic of Modalities (1930): Translation, Commentary and Analysis*, Synthese Library**444**, Springer (2022) [doi:10.1007/978-3-030-87548-0]

added pointer to:

- E. John Lemmon with Dana Scott,
*An Introduction to Modal Logic – The “Lemmon Notes”*, B. Blackwell (1977) [ark:/13960/t3gz25k3h]

I ended up making a fair bit of adjustments to the wording in the Idea-section (here).

Generally, i find that our entries on modal logics leave much room for improvement, but I’ll leave it at this for the moment.

]]>I have added publication data and hyperlinks to these previously existing bibitems:

Patrick Blackburn, Maarten de Rijke, Yde Venema,

*Modal Logic*, Cambridge Tracts in Theoretical Computer Science**53**(2001) [doi:10.1017/CBO9781107050884]Patrick Blackburn, Johan van Benthem, Frank Wolter (eds.),

*The Handbook of Modal Logic*, Elsevier Amsterdam (2007) [book webpage, publisher page]

and then I added this further textbook pointer:

- Raymond Bradley, Norman Swartz,
*Possible Worlds – An Introduction to Logic and its Philosophy*Hackett Publishing (1979) [pdf]

I added in some common modal axioms. Could do with some commentary.

]]>That’s a point. The full quote from #79 comes after acknowledgement of the advantages of toposes over ionads, and then says:

…yet there remain good reasons for having the notion of ionad available to us. The first is that some particular applications of topos theory may be more perspicuously expressed in the language of ionads than of toposes: two examples that come to mind are the sheaf-theoretic semantics for first-order modal logic given in [1], and the generalised Stone duality of [5]. The second reason is pedagogical. Many aspects of topos theory are abstractions of corresponding aspects of general topology, but the abstraction is twice removed: first one must pass from spaces to locales, and then from locales to toposes. At the first step, one loses the points, which to many, is already to enter a quite unfamiliar world, and the second step can only compound this unfamiliarity. With the notion of ionad available, one may arrive at these same abstractions by a different route, passing first from spaces to ionads, and then from ionads to toposes. The advantage of doing so is that one retains the tangibility afforded by the presence of points for as long as possible. It seems to me that it is in this pedagogical aspect that ionads are likely to make their most useful contribution.

Hmm, maybe not too advantageous then.

]]>I would have to look at Garner’s article to see what he claims might be gained by such terminology.

I suppose he proves something about finite limit perserving comonads that has not been noticed elsewhere before?

]]>Where would it take us then if we declare:

An $\infty$-ionad is given by an $\infty$-groupoid, $X$, and a finite $\infty$-limit preserving comonad, $I_X: \infty Grpd/X \to \infty Grpd/X$?

Then we could have:

The $(\infty, 1)$-category of opens $O(X)$ of an $\infty$-ionad $X$ is the category of $I_X$-coalgebras.

This would be an $(\infty, 1)$-topos.

Presumably there would be no reason to stick to $\infty Grpd$ as the base topos.

]]>Well I’d still like to know the ’meanings’ of the comonad, $i^\ast \circ i_\ast$, and monad, $i^\ast \circ i_!$, on $\mathbf{H}/\flat X$. Is there something like an ’interior’ for a topology happening in the former? Is the analogue of putting a topology on a set just to locate a type with given image under $\flat$? Do analogues of the ionads paper work out, e.g., section 3 on generalized bases?

Maybe in a more speculative direction, if we follow Garner

there remain good reasons for having the notion of ionad available to us. The first is that some particular applications of topos theory may be more perspicuously expressed in the language of ionads than of toposes: two examples that come to mind are the sheaf-theoretic semantics for first-order modal logic given in [1], and the generalised Stone duality of [5],

then perhaps if Awodey et al. show that their sheaf semantics is complete for first order S4 modal logic, we can start to see why this is so from the larger perspective of slice $\infty$-toposes, or say something similar about modal type theory?

And there may be a higher models-theory duality, maybe for type theories, along the lines of First-Order Logical Duality and Scheme representation for first-order logic.

]]>you professionals could probably sort it out between you in 15 milliseconds

Maybe you could highlight again what exactly you’d like to see sorted out.

My impression was you already found the analogy you wanted in #74:

so the analog of the category $Set^X \simeq Set_{/X}$ of $X$-indexed sets is the slice $\mathbf{H}_{/X}$ for any object $X$ in the $\infty$-topos $\mathbf{H}$. Now you are asking for finite $\infty$-limit preserving comonads on such slices. You get one such by base change along any morphism out of $X$.

This establishes the analogy to ionads. In particular jets would be an example. Now what I don’t know is what that analogy tells us, if anything.

]]>Right, I’d better go and do something else. I’m getting more whiffs that something ionad-ish is going on when the base is set-like, and perhaps there might even be flat bundle-valued differential forms about. But you professionals could probably sort it out between you in 15 milliseconds, and I need to write some philosophy papers.

]]>Oh, I see. That’s of course, true, too.

]]>Just to clarify, my initial thought was that we had a case already of the operation of $i^{\ast}$:

$i^{\ast} (\ast \to \mathbf{B} G) = (\flat_{dR}\mathbf{B}G \to \flat \mathbf{B}G).$ ]]>Oh, I see. I though we were just working out $i^{\ast}$, and that that would have an existing name as something which flattens. But perhaps it’s easier to go for the composite straight away. I’ll go back and read with that in mind.

Presumably it’s possible that composing the other way is interesting $i_! \circ i^\ast$, but all seems to point to the other way,

An

ionadis a set $X$ together with a finite limit-preserving comonad $Int_X$ on the category $Set^X$

chimes with

In the original expression, we consider the geometric morphism from the topos $Sets/|X|$ of sets indexed over a set $|X|$ to the topos $Sh(X)$ of sheaves over a topological space induced by the (continuous) identity map $id: |X| \to X$. The modal operator $\Box$ is interpreted by the interior operation $int$ that the comonad $id^{\ast} \circ id_{\ast}$ induces on the Boolean algebra $Sub_{Sets/|X|}(id^{\ast} F) \cong \mathcal{P}(F)$ of subsets of $F$.

[EDIT: These are, of course, using the right adjoint to $i^\ast$, but still the interest is starting out from the discrete side.]

]]>then why do you have $\flat B$ in both corners of that square?

I thought that’s what you were suggesting to look at. The operation $i^\ast \circ i_!$ in your #67 above is the operation that sends any $\phi \colon X \to \flat B$ to the pullback

$\array{ &\longrightarrow& X \\ {}^{\mathllap{i^\ast i_! \phi}}\downarrow && \downarrow^{\mathrlap{\phi}} \\ && \flat B \\ \downarrow && \downarrow \\ \flat B &\longrightarrow& B } \,.$I thought your point in #68 had been to observe that then the $\flat_{dR}$-operation becomes sort of a special case of the possibility-like modality $i^\ast \circ i_!$, via

$\flat_{dR} B = \ast \underset{\flat B}{\times} i^\ast i_! id_{\flat B} \,.$ ]]>Well I just meant that there’s some process which takes us from some bundle $X \to B$ to some other bundle $Y \to \flat B$. Wouldn’t we call that a ’flattening’.

Anyway, I was with you so far, but then why do you have $\flat B$ in both corners of that square?

]]>You mean: to pick trivial underlying $\infty$-groupoid $\infty$-bundles.

Consider first pointed connected coefficients, hence of the form $\mathbf{B}G$. Then the homotopy pullback $\flat_{dR}\mathbf{B}G$

$\array{ \flat_{dR}\mathbf{B}G &\longrightarrow& \flat \mathbf{B}G \\ \downarrow &\swArrow& \downarrow^{\mathrlap{\chi}} \\ \ast &\longrightarrow& \mathbf{B}G }$has the following interpretation: its generalized elements consist of

a flat connection $\nabla \in \flat \mathbf{B}G$ with underlying bundle $\chi(\nabla) \in \mathbf{B}G$;

an equivalence $\ast \simeq \chi(\mathbf{B}G)$.

Hence it’s a flat connection equipped with a trivialization of the underlying bundle. Classically this is the same as a flat (closed) differential form.

Now as you generalize this from the pointed connected $\mathbf{B}G$ to any $B$, then $B$ has the interpretation of classifying groupoid principal bundles. Now there is not a single trivial such, but there is one trivial such for each connected component of $B$. You may choose to pick all of these connected components and all of the transformations between them, and then consider the homotopy pullback $Q$ in

$\array{ Q &\longrightarrow& \flat B \\ \downarrow &\swArrow& \downarrow^{\mathrlap{\chi}} \\ \flat B &\longrightarrow& B } \,.$Clearly this has *some* relation to $\flat_{dR}$. I suppose if one picks one representative points in each connected component of $B$ and hence pulls back along some $\pi_0(\flat B) \longrightarrow \flat B$, then one obtains the “right” definition of $\flat_{dR}$ for groupoid-principal connections.

Right now I am not sure what it means to retain all the higher homotopy information of the $\flat B$ in the bottom left corner.

But I agree that this looks like a sensibel perspective from which to view $\flat_{dR}$ in generality.

]]>The must be a universal way to flatten a connection on an $\infty$-bundle.

]]>So $\flat_{dR}$ is supposed to be defined on pointed objects, and then the pullback is along the one canonical basepoint. But of course you have a point here that in the absence of a choice of such a basepoint, then it may make sense to call the construction that you are considering here a generalized $\flat_{dR}$-construction.

]]>It would probably be better for the soul to work this out myself.

So $i_!$ is a forgetting of the flatness of a connection.

Then $i^{\ast}$ provides a pullback, so is a general version of the dR-flat modality.

]]>I was trying to work out some of the modalities to arise from those modalities we know and love via base change and adjoints. If you consider the eleven (non-identity) modalities of the cohesion - table, then for each one there is the corresponding (co)unit. For a given object, $X$, we can then base change along the (co)unit and form its left and right adjoint. These in turn can be composed to generate four (co)monads.

Why consider these 44? Well we have 6 data points that some are interesting.

- The monad $\ast$ and $X$ a set: necessarily, possibly, reader monad, writer comonad.
- The monad $\Im$: jet comonad, infinitesimal disk bundle,…

So I’d like to work out some others.

As I said above, there might be something useful to do with the counit of the comodality $i: \flat(X) \to X$?

$(i_! \dashv i^\ast \dashv i_\ast) \;\colon\; \mathbf{H}_{/\flat (X)} \stackrel{\overset{i_!}{\longrightarrow}}{\stackrel{\overset{i^\ast}{\longleftarrow}}{\underset{i_\ast}{\longrightarrow}}} \mathbf{H}_{/X} \,.$Again four (co)monads from the composites. Can we name any of them?

]]>