# Start a new discussion

## Not signed in

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

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTim_Porter
• CommentTimeOct 19th 2010

I have started modal logic, and relational structure. Here my eventual aim will be to see if there is an n-POV version of some of the modal logics. (This was discussed some time ago on the Café I seem to remember.) For that I am trying link it to higher transition systems and various other things. I will probably do some exploration on my personal pages a bit later on but for the moment am just getting basic stuff down on the Lab.

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeOct 19th 2010

There certainly seems to be a coalgebraic flavour to modal logic. And then there’s also the sheaf semantics point of view (see same post).

• CommentRowNumber3.
• CommentAuthorTim_Porter
• CommentTimeOct 19th 2010

@David I have been quietly increasing (slowly) the coalgebraic related stuff with a view to pushing that link further.

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeOct 19th 2010

It would be great if you could make any sense of the intuition I had there relating Awodey’s sheaf semantics for first-order modal logic and the coalgebraic treatment of modal logic. What I have most come to admire about mathematicians is their willingness and ability to pursue a line of research, when the target is only glimpsed through the mists, and may yet turn out to be a chimera.

• CommentRowNumber5.
• CommentAuthorTim_Porter
• CommentTimeOct 19th 2010

@David. What I see is more of a Cerberus or Hydra, with many heads on the single body. (There is a three headed dog under a window of a lodge house in Bangor.)

• CommentRowNumber6.
• CommentAuthorTim_Porter
• CommentTimeOct 19th 2010

My queries are silly ones such as ’What would be the higher dimensional language accepted by a higher dimensional automaton?’

• CommentRowNumber7.
• CommentAuthorTim_Porter
• CommentTimeOct 19th 2010
• (edited Oct 19th 2010)

Naming question: The usual name for the models of a modal logic is ’frame’, usually Kripke frame, but the attribution to Kripke is another example of Baez’s law and others such as Richard Monatgue, Hintikka and ’others’ were also influential at the same time in the introduction of relational semantics. I have called them frames (Kripke), but feel that is awkward. Perhaps Kripke frame is the solution. Opinions.. if there are any.

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeOct 19th 2010

As for the name of the page, I think “frame (modal logic)” would be appropriate (perhaps a disambiguation page for “frame” would be good as well), but calling them “Kripke frames” in the text seems like a fine idea. Does anyone else refer to them as such?

• CommentRowNumber9.
• CommentAuthorTim_Porter
• CommentTimeOct 19th 2010

There is at present only a mention of them as I have not created the entry and will wait for a while to get reactions.

Does anyone else refer to them as such?

Lots of people in the Modal logic literature do. There are only references to Kripke-Joyal semantics on the n-Lab.

• CommentRowNumber10.
• CommentAuthorTim_Porter
• CommentTimeOct 19th 2010

I looked up general frame in Kracht’s book and he takes a frame to be a set with a family of relations and a Kripke frame to be the special case when the relations are all binary ones. That may be a solution but it also suggests a question. The binary case (used for epistemic and temporal logics, for instance) uses binary relations and hence Kripke frames. The temporal logics use a single modal operator (more or less) and the Kripke frames then use a $\le$. The epistemic logics use multi-equivalence relations for their models. Perhaps n-dimensional situations require relations that are (n+1)-ary.

• CommentRowNumber11.
• CommentAuthorTim_Porter
• CommentTimeOct 19th 2010

I have renamed things as frame (modal logic) with the term ’frame’ used where no ambiguity seems likely. We can use Kripke frames as I will put some redirects.

• CommentRowNumber12.
• CommentAuthorTobyBartels
• CommentTimeOct 21st 2010
• (edited Oct 21st 2010)

I don’t see why we can’t say ‘Kripke frame’, up to and including the title of the page. That’s what people call them, and it’s unambiguous (unlike ‘frame’) and easy to use (unlike names with parentheses). Baez’s Law is no excuse for avoiding a handy name.

By the way, I added these to the list at Baez’s law, using the text from Tim’s comment. But maybe you can make that clearer, Tim?

• CommentRowNumber13.
• CommentAuthorTim_Porter
• CommentTimeOct 21st 2010

The names associated to this relational semantics include Prior (loads of puns here). He introduced a relational semantics for tense logics also called temporal logics earlier than Kripke so has the priority …. and so on! It all happened about 1957 and in Blackburn, de Rijke and Venema there is a longish historical overview. (By the way their book is very nice to read and to me is very interesting.)

1. Perhaps this is an obvious point, but I’ve always thought of the coalegebraic connection as arising from the fact that frames are typically some form of closure of a relation, and the standard modal operators like box and diamond can only refer to properties that hold of the closure.

So suppose $W$ is the set of worlds, and we have a relation $R \subseteq W \times W$. Now, suppose our frame $F$ arises as the transitive closure of $R$. Then a proposition like $\Box A$ holds at a world $w$ if $A$ holds in every world reachable from $w$. Now, the point is that $\Box A$ can’t distinguish between two relations $R$ and $S$ which happen to have the same transitive closure. That is, if $R^*$ and $S^*$, viewed as the big-step transition systems induced by the closure operation, are bisimilar, then they will prove the same formulas.

• CommentRowNumber15.
• CommentAuthorTim_Porter
• CommentTimeOct 21st 2010

@Neel The transitive closure will only be relevant, I think, if the logic satisfies the axiom usually denoted (4), as in S4, etc. Perhaps I am wrong.

I do intend to look at the coalgebraic notion as I go through the theory. Also the algebraic Boolean algebras with operator models, and related ideas are on the list of things to add.

Do keep checking that I don’t get things wrong! :-)

• CommentRowNumber16.
• CommentAuthorDavid_Corfield
• CommentTimeOct 21st 2010

The matching of conditions on R to the different systems of modal logic is done pretty well on the Wikipedia page.

You can see how you might not want transitivity in a modal logic, such as epistemic logic. I may know P but not know that I know P. Good exercise to encode Rumsfeld’s

There are known knowns; there are things we know that we know. There are known unknowns; that is to say, there are things that we now know we don’t know. But there are also unknown unknowns; there are things we do not know we don’t know.

Actually he missed the interesting fourth, unknown knowns, unless he holds the KK principle, i.e., transitivity.

• CommentRowNumber17.
• CommentAuthorTim_Porter
• CommentTimeOct 21st 2010

My ’secret agenda’ is to look at all the modal logic aspects of transition systems, multiple equivalence relations etc., and then to see if there is any hope of getting higher dimensional transitions systems, etc. to give something like a language or a logic or an algebra (BAO). (For instance, the trace semantics of transition systems with independence is really the fundamental category construction of directed homotopy.) I have no idea if it will work or not but intend to have some fun in tracking it through. (and anyone else is welcome to join me).

A second agendum item is that I hope that putting a bit more of the stuff that reflects both the nPOV and interacts with Theoretical Computer Science, logic and philosophy may (i) increase the usefulness of the Lab to workers in those disciplines and (ii) get some of the people with expertise in those areas to join the construction team or at least make helpful comments here in the Forum, and occasionally correct any faux pas in the entries. The nLab pages are intended as the Lab book of a group of interacting people, so the modal logic entries are my scribblings to try to get back what I understood a few years ago!

• CommentRowNumber18.
• CommentAuthorDavid_Corfield
• CommentTimeOct 21st 2010

Great, I’ll certainly try and chip in. There must be something to the thought that the next stage up from the accessibility relation between worlds (Is w’ accessible or not?) is ’How is, or what is the set of ways in which, w’ is accessible?’. Instead of the coalgebra map $W \to P(W)$, corresponding to the relation $R$ on set of worlds $W$, we have a $C \to Presheaf(C)$, which to every world in category of worlds $C$ gives the functor $C^{op} \to Set$ of accessibility. Seems to be a kind of 2-coalgebra.

• CommentRowNumber19.
• CommentAuthorTim_Porter
• CommentTimeOct 21st 2010

Interesting. yes that is worth following up. One thing I noted above is the trace semantics interpretation. If you look at Winskel on transition systems then the independence of a and b seems to correspond to creating a 2-d model of the system. I tried looking up trace semantics in general but got lost in the wide variety of places it occurs (Paul André Mellies has some nice things on it I noted.). I need to take apart the coalgebra treatment and the idea of covarieties as well. I had a lot of stuff on this but threw some of it away not long ago….! When you do that it is sure that you are going to find a need for it later. I have to retract away from my Bangor office gradually and have not the space at home for everything. I have electronic copies of some of it (Alex Kurz’s notes are nice.)

The S5 models are equivalence relations on the set of worlds so groupoids would again seem the thing to think of there.

• CommentRowNumber20.
• CommentAuthorTim_Porter
• CommentTimeOct 22nd 2010

I have split off geometric models for modal logics from the corresponding entry on frames. The previous page seemed likely to get confusing if I added in all that was need on frames.

I came to the conclusion that using Kripke frames when the relations are binary and frames in general was probably the best naming scheme.

I started temporal logic and would love it if someone felt like contributing more there. I left tense logic as an unfilled link as I am not sure if that is worth expanding. I find it very interesting as it relates to verbal handling of time. It is not quite the same as temporal logic or so it seems).

• CommentRowNumber21.
• CommentAuthorDavid_Corfield
• CommentTimeOct 22nd 2010

I seem to remember that there are ways to specify the density of temporal instants, noncircularity, nonbranching, continuum nature of time, etc.

Modalities get quite tricky even in everyday language:

In a seemingly simple piece of knowledge such as ‘Normally, the likelihood of road congestion is smaller on weekends’, one implicitly makes use of default logics (‘normally’), probabilistic reasoning (‘the likelihood’) and temporal knowledge (‘weekends’) under a quantitative regime (‘smaller’).

• CommentRowNumber22.
• CommentAuthorTim_Porter
• CommentTimeOct 22nd 2010

My plans for the moment are to develop basic temporal logic a bit more (possibly with ’until’), but the idea of specifying the density of temporal instants sounds a good idea to put in. As I said, my agenda is to understand ’time’ here but eventually to see if it can be tied in to directed homotopy etc. For that non-circularity, non-branching etc, may be well worth developing.

For other purposes I think these modal logic pages are worth having but (as Wikipedia does quite a nice job on this) it would be good to develop in new directions as well. The probabilistic stuff would be interesting if you can find it (and summarise it?). My feeling is that a probabilistic eement is essential for several of the entries elsewhere, e.g. directed homotopy, and I am not sure how that should go (at all)!

I have a bit more to put in to temporal logic but also have to add to various of the other entries in the family.

• CommentRowNumber23.
• CommentAuthorTim_Porter
• CommentTimeOct 22nd 2010

I forgot to mention bounded morphisms that are clearly fibrations in all but name.

• CommentRowNumber24.
• CommentAuthorDavid_Corfield
• CommentTimeOct 22nd 2010

Digging out a student essay, I have the claim that

($F \top \wedge q \wedge H q) \to F H q$ represents discreteness.

Let’s see, if there is a future moment, q is true now and has been until now, then there is some time in the future when q has always been true.

$F q \to F F q$ represents density.

If q will at some point in the future be true, then there’s some time in the future when q will be true in the future.

• CommentRowNumber25.
• CommentAuthorTim_Porter
• CommentTimeOct 22nd 2010

I have the density thing in there already. (It is discussed in Blackburn et al.) I’m not sure that the use of ’density’ really captures that. It was said that between any two times there was a third, but if a time has no proposition true at it, is it detectable? (My observation model is kicking here.) That seems vaguely disquieting to me for the density interpretation.

• CommentRowNumber26.
• CommentAuthorTim_Porter
• CommentTimeNov 1st 2010
• (edited Nov 1st 2010)

@David Can you add anything from that to the temporal logic entry and suggest anything that more should be said there. (Do you know the link between temporal logics and S4? The sources that I have tend to emphasise the epistemic rather than the temporal side of things.)

• CommentRowNumber27.
• CommentAuthorTim_Porter
• CommentTimeNov 3rd 2010
• (edited Nov 3rd 2010)

I have added the logic T(m). The title is awkward since there does not seem a neat title that reads well (ideas anyone… and I have K, (done), S4 and S5 coming up!!!!) moreover it should be $T_{(m)}$ but that does not work in a title due to the latex.

More interestingly, I have given the simple proof that the frames that model the $T$ axiom are precisely the reflexive frames, i.e. that they consist of a set together with a reflexive relation on it or more generally with $m$ reflexive relations on it.

(Edit: When proving that I was thinking, how does one do all this in a more constructive or intuitionistic setting? )

• CommentRowNumber28.
• CommentAuthorTobyBartels
• CommentTimeNov 4th 2010

I’m not sure why you can’t just call it T(m). Does that mean anything else?

In any case, may be I so bold as to suggest that you use the title atop the contents listing to get a properly formatted title for the page? I have put this in; see how you like it.

• CommentRowNumber29.
• CommentAuthorTim_Porter
• CommentTimeNov 4th 2010

@Toby I was just admiring it. :-)

For the name, you may have a point. I was trying to keep in with some of the sources, but the naming in the three books that I am consulting is not uniform! I will hit the same ’problem’ with S4(m) and S5(m) and neither would seem to cause difficulties.

• CommentRowNumber30.
• CommentAuthorTim_Porter
• CommentTimeNov 12th 2010
• (edited Nov 12th 2010)

I have been continuing my ’nibbling away’ at modal logics with an aim of revealing pieces of a jigsaw which just might give me a hint at how to categorify this stuff and logic in general. My latest foray has written a short entry on closure algebras. These provide the algebraic semantics for the modal logic S4. The open elements in a closure algebra form a Heyting algebra and we know how to categorify that. Any Heyting algebra is isomorphic to such an algebra of open elements. (I have not given a proof, but suppose it to be more or less obvious, (I hope)). The dual Kripke semantics of S4 is given by preorders.

How can one categorify this situation? Any thoughts however banal would be welcomed. (The intuitionistic version of S4 has a semantics in terms of simplicial sets! (to be checked up on in the paper by Eric Goubault and his brother.) Categorifying preorders should be ’simple’ but what is the corresponding ’algebra’.

I next turn to monadic algebras (still to be constructed). My side reading says these are useful in classical situations (i.e. non-modal ones), but that will need input from someone else. These model S5 and the Kripke semantics of S5 is via equivalence relations. There one could replace the relation by a groupoid. (S5(n) would then give a multiple groupoid.)

The dualities between Kripke and modal algebra approaches are all extensions of the ultrafilter Stone duality set up. I would expect to see cogroupoid emerging within the algebraic context, but as yet I don’t.

Edit: Stub of monadic algebra created.

Edit2: The Goubault paper deals with intuitionistic S4 proof term semantics. That would accord well with vague intuitions that in S4 and S5 we first have to interpret the relation as a reason or proof that something happens and there may be more than one reason. (WILD GUESS: SImplicially enriched categories may be what is needed!)

• CommentRowNumber31.
• CommentAuthorTim_Porter
• CommentTimeNov 14th 2010
• (edited Nov 14th 2010)

@David in no 16. I found this on the web. I have not checked his section on Rumsfeld logics yet. (My download time on a Sunday afternoon is BAD!)

For everyone, this seems to show that somewhere modal logics are being taught to sociologists (and quite right to). I doubt that this is the case in the UK.

I have put a query box on the logic S5(m), and would love some thoughts.

• CommentRowNumber32.
• CommentAuthorDavid_Corfield
• CommentTimeNov 16th 2010

Sorry for not joining in on this. I’m horribly busy at the moment. I seem to have got myself roped into heading the department next term. But I’ll took a look when I can.

• CommentRowNumber33.
• CommentAuthorDavid_Corfield
• CommentTimeMar 9th 2011

If somebody in the future comes back to this discussion, I hope they’ll take a look at this post and comments. I feel sure we should be pursuing ionads for first-order modal logic.

• CommentRowNumber34.
• CommentAuthorTim_Porter
• CommentTimeMar 9th 2011

I think Steve Awoday’s ideas look good. I found the paper the other day (whilst looking for something else!). What I return to, however, is my feeling that somehow, we are all missing some simple point about what ‘n-categorical modal logics’ should be. (I think I said that ionad was the first use of Irish in our mathematical area. (Welsh already has appeared. As an aside, can anyone give another Irish term used in maths., etc. Finn any ideas? also what is the Welsh word? and why?))

• CommentRowNumber35.
• CommentAuthorFinnLawler
• CommentTimeMar 9th 2011

The CS people here often give Irish names to things like software and protocols, but I can't think of any other Irish words used in maths. The only Welsh word I know is tas, for 'stack', I think. I saw it in Crans's thesis.

This connection between modal logic and coalgebra is one that I've been meaning to look at for ages, especially since Matthew Hennessy came to our research group. Hennessy--Milner logic must be the primordial link between the two areas. Is it talked about in the modal logic literature much?

• CommentRowNumber36.
• CommentAuthorTim_Porter
• CommentTimeMar 9th 2011

Of course, the first recorded use of the symbol $\pi$ for 3.1415…. is in the work of a Welsh mathematician, but Cymru cannot claim that pi itself is Welsh. Crans use of Teisi (plural of tas I think) was what I was thinking of.)

I probably need to mention modal logic to people down in Swansea, as they are well into coalgebraic stuff and I will be visiting there to give a talk later this month.

• CommentRowNumber37.
• CommentAuthorDavid_Corfield
• CommentTimeMar 10th 2011

Re. 34

we are all missing some simple point about what ’n-categorical modal logics’ should be…

Well, it could be said that we don’t even know what 2-categorical ordinary logic should be, although Mike looks like he’s on track.

At least we should systematise the formation of the modal counterpart of a logical language. So propositional logic is about sets of models (lines in a truth table) for a propositional theory. The modal logic takes such a set, $X$, and either works via a frame $X \to 2^X$, or else via a map $2^X \to 2^X$ which may be the interior operation on a subset.

We ought to play the same game with $X \to Set^X$ and $Set^X \to Set^X$.

• CommentRowNumber38.
• CommentAuthorDavid_Corfield
• CommentTimeMar 10th 2011

There ought to be something like a situation where you have worlds, and then for any two worlds a set of ways in which the second is accessible to the first. This generalises the accessibility relation from whether to how: $X \to Set^X$. Then it could matter which way you get from one world to another. In the propositional case, take $w_0$ and $w_1$, where we can access the second from the first but not the other way around. Then we have $\Box P$ true at $w_0$ if $P$ holds at both worlds.

Imagine now there are two ways of getting from $w_0$ to $w_1$. Let’s move up to the first order case where at each world we have a set of individuals and the access paths between worlds induce mappings between individuals, called their counterparts. Let’s say we have two individuals at each world, but the counterparts according to the two paths do not coincide. If precisely one individual in each world has property $P$, then we would have the situation where $\Box \exists x P(x)$ holds at $w_0$ according to one path, but not the other.

There would have to be a way of distinguishing between ’there is some way in which this is necessarily true’, and ’in every way this is necessarily true’.

• CommentRowNumber39.
• CommentAuthorTim_Porter
• CommentTimeMar 10th 2011

This is similar to my naive idea (for S5) of replacing the equivalence relation as a model by a groupoid. I wrote an article where I looked at this where locally things were represented by groupoids but different worlds might be accessible by various paths defined locally. This gets really interesting in the multiagent system setting where strange things seem to happen. (e.g. in modelling Muddy children!)

Perhaps we have a situation where a path corresponds to a string of arguments, one string of arguments may imply that P is true, whilst another string may not although it seems to relate the same two worlds. The validity if each part of the string is local, which explains why it is path dependent. This then gets near to the sort of programming problems encountered in concurrent programming, and to Eric Goubault’s original ideas on directed homotopy.

• CommentRowNumber40.
• CommentAuthorMike Shulman
• CommentTimeMar 10th 2011

I don’t have time to work through this myself right now, but I agree that whatever propositional modal logic is doing with the interior operator of a space should correspond in the Awodey-Kishida model of first-order logic to the comonads used to define ionads.

• CommentRowNumber41.
• CommentAuthorDavid_Corfield
• CommentTimeMar 10th 2011

In the propositional case, you have two pictures for the accessibility relation:

Either, a frame (relation) $R: X \to 2^X$, or, an operation on subsets of $X$, $A \mapsto \{x \in A| x R y \Rightarrow y \in A\}$.

If $R$ is at least reflexive and transitive, the operation on subsets is an interior operator, and we get topological semantics for propositional S4. But you can have lots of fun with more general frames.

It seems that we’re seeing in Awodey-Kishida+ionads the first-order S4 through the eyes of an interior operator, $Sets^X \to Sets^X$. That leaves me wondering about the corresponding general frames $X \to Sets^X$. Is there a slick arrow-theoretic way to characterise the passage from the relation $R: X \to 2^X$ to the operation on subsets of $X$, $A \mapsto \{x \in A| x R y \Rightarrow y \in A\}$?

• CommentRowNumber42.
• CommentAuthorTim_Porter
• CommentTimeMar 10th 2011

@David I am not sure what you are asking for here. Something like a comma category seems to be what is going on, but that seems very superficial as a comment, so I suspect I am not looking deeply enough.

• CommentRowNumber43.
• CommentAuthorDavid_Corfield
• CommentTimeMar 10th 2011

I was just wondering how to analogise the mechanism from frame to topology, to one between some kind of $X \to Sets^X$ and ionads. Trying to understand Garner’s paper, part of the story is that given a certain kind of $M: X \to Sets^X$, one can place a category structure, $C$, on the set $X$, such that $Hom_C(x, y) = M(x)(y)$. Then the interior operation takes $Sets^X$ to $Sets^C$.

• CommentRowNumber44.
• CommentAuthorUrs
• CommentTimeNov 4th 2011
• (edited Nov 4th 2011)

Hi all you modal logicians,

I would like to have a decent Idea-paragraph at modal logic.

I know that the current version says “under construction”, but it is a bit off-putting that a layman (I am such a layman) can read screen-wise into this entry without getting from it the faintest idea of what modal logic actually is.

In modal logic the usual logical operations (and, or, forall, etc) are accompanied by a few more operators – called the modalities – that express the idea that some propositions may be true “in a certain way”. The classical example is a system that means to model the idea of propositions being “possibly true” or “necessarily true”. But other kinds of modalities can be considered, too.

Some expert please check if that makes sense, or improve where necessary. Then we can insert something like this into the Idea-section of the entry.

• CommentRowNumber45.
• CommentAuthorMike Shulman
• CommentTimeNov 5th 2011

That looks reasonable to me, but I’m not really a modal-logician as such.

• CommentRowNumber46.
• CommentAuthorTim_Porter
• CommentTimeNov 5th 2011
• (edited Nov 5th 2011)

I am adapting that and adding more. (I am not a modal logician either!;-))

(a bit later: I have tried to give a bit more idea. Is more needed?)

• CommentRowNumber47.
• CommentAuthorTim_Porter
• CommentTimeNov 5th 2011
• (edited Nov 5th 2011)

I have created a stub for provabilty logic, just giving a link to the Stanford Encyclopedia entry, and have provided a link to their modal logic entry, in our modal logic entry.

• CommentRowNumber48.
• CommentAuthorUrs
• CommentTimeNov 5th 2011

Thanks, Tim!

I have slightly edited the Idea-section further. Please have a look to see if you can live with it.

Then I have added a brief paragraph titled Modal logic – categorical semantics that refers to the interpretation of modalities as (co)reflectors.

• CommentRowNumber49.
• CommentAuthorDavid_Corfield
• CommentTimeNov 5th 2011

Made one or two changes, but had less time than I thought, so will have to come back later.

• CommentRowNumber50.
• CommentAuthorTim_Porter
• CommentTimeNov 5th 2011

I have not checked who made what changes, but I like the way the ideas section is shaping up.

• CommentRowNumber51.
• CommentAuthorUrs
• CommentTimeOct 24th 2012

I am gradually discovering lots of well hidden $n$Lab entries on topics in modal logic.

Let’s point to them prominently from the entry modal logic in a way that makes it possible to find them before one knows that they exist.

Probably there are more entries that could go there. Who knows about them. Tim?

• CommentRowNumber52.
• CommentAuthorTim_Porter
• CommentTimeOct 24th 2012

There was a list of types of modal logic put there. I have duplicated it so the examples list can be expanded a bit. Can someone write a little on constructive modal logics or intuitionistic ones because I am ignorant on these (and do not claim great knowledge on the others either.:-))

• CommentRowNumber53.
• CommentAuthorUrs
• CommentTimeOct 24th 2012
• (edited Oct 24th 2012)

Can someone write a little on constructive modal logics or intuitionistic ones

Well, that’s what the entry modal type theory is about. The logic in modal type theory is constructive intuitionistic modal logic.

But of course all that deserves to be discussed further…

• CommentRowNumber54.
• CommentAuthorTim_Porter
• CommentTimeOct 24th 2012

The entries were put there and announced! At that time modal logics were well down priority lists so did not get above the event horizon. (I was merely trying to fill in some background since the monads in computer science entry did not mention the coalgebraic stuff). I like modal logics b’cos they are fun to work with and useful. Happy reading… the transition systems stuff of Kurz and others goes off into Markov systems etc so that ties back into another thread.

• CommentRowNumber55.
• CommentAuthorTim_Porter
• CommentTimeOct 24th 2012

In case this helps for the semantics vs. syntax discussion, there is an entry on the Lindenbaum-Tarski algebra of a normal modal logic.

• CommentRowNumber56.
• CommentAuthorTim_Porter
• CommentTimeOct 25th 2012

I just came on a paper by Mai Gehrke here, that may be of interest.

• CommentRowNumber57.
• CommentAuthorUrs
• CommentTimeNov 6th 2012

I have added relevant material that people have been mentioning on the $n$Forum to modal logic.

In the course of this I have re-arranaged the entry a bit. The Idea-section used to be long and unfocused. I have shortened it drastically by moving paragraphs to further below in the relevant Properties- or Examples-section.

In the Examples-section I have merged the list of flavors of modalities that used to be there with what David had posted elsewhere. Then there is now a subsection with further details on epistemic logic. Though maybe that should go to epistemic logic. It is quite a bit rough anyway.

• CommentRowNumber58.
• CommentAuthorTim_Porter
• CommentTimeNov 6th 2012

I agree that the section on epistemic logic does not fit well here. I will take it over to the appropriate entry.

I also will check up on the coalgebraic modal logic as that might live better in a separate section. I feel a link labelled coalgebraic semantics would look good, but there is also a possibility of coalgebraic modal logic as a form of modal logic. I will try it out after checking up o a few things.

• CommentRowNumber59.
• CommentAuthorTim_Porter
• CommentTimeNov 6th 2012

I have started an entry coalgebraic model for modal logic, but have just a stubby ideas section as yet. I edited modal logic as I suggested and I think it looks a bit cleaner. We can always go back to the old form if that seems better.

I cut the epistemic logic bit out of modal logic and inserted it as an idea section in epistemic logic.

• CommentRowNumber60.
• CommentAuthorDavid_Corfield
• CommentTimeNov 7th 2012

Split off first-order modal logic, but no time to do anything substantial.

• CommentRowNumber61.
• CommentAuthorUrs
• CommentTimeMar 13th 2013
• (edited Mar 13th 2013)

Chasing references that David Corfield pointed to elsewhere, I realized that the Stanford Encyclopedia of Philosophy has (at least) two entries on modal logic. Earlier I had only seen the one titled Modal logic but now I see there is also Modern Origins of Modal Logic. The second one is well suited as first reading/motivation for the first one, I find.

So I went and added a pointer to this prominently right in the idea-section of modal logic. In the course of this I also ended up editing the Idea-section a little bit more.

• CommentRowNumber62.
• CommentAuthorzskoda
• CommentTimeMar 19th 2013

Link to the paper of Goldblatt at modal logic does not work.

• CommentRowNumber63.
• CommentAuthorTim_Porter
• CommentTimeMar 20th 2013

It does now. There was an http:// missing.

• CommentRowNumber64.
• CommentAuthorUrs
• CommentTimeSep 3rd 2015
• (edited Sep 3rd 2015)

have added to modal logic the reference

• Dana Scott, Advice on Modal Logic, in Karel Lambert (ed.) Philosophical problems in Logic – Some recent developments, Reidel 1970

and the quote (p. 161)

Here is what I consider one of the biggest mistakes in all of modal logic: concentration on a system with just one modal operator.

• CommentRowNumber65.
• CommentAuthorDavid_Corfield
• CommentTimeJun 14th 2016
• (edited Jun 14th 2016)

To return (after a long while) to ionads and modal logic (#33 and #40), looking back at the quote in the post linked from (#33) from Awodey and Kishida:

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$,

it sounds reminiscent of the $\flat$ modality. Did we ever consider using other units/counits of our favourite modalities?

I mean, we noted the similarity between the jet comonad and ordinary necessity as arising from units of modalities, $\Im$ and $\ast$, in Urs’s cohesion - table:

$Jet \coloneqq i^\ast i_\ast \;\colon\; \mathbf{H}_{/X} \to \mathbf{H}_{/X} \,.$

and

$\Box_W: \mathbf{H}_{/W} \to \mathbf{H}_{/W} \,.$

What could we do with the counit of the comodality $i: \flat(X) \to X$?

$\mathbf{H}_{/\flat (X)} \stackrel{\overset{i^\ast}{\longleftarrow}}{\underset{i_\ast}{\longrightarrow}} \mathbf{H}_{/X} \,.$

So we have $i^\ast i_\ast$ again acting on $\mathbf{H}_{/\flat (X)}$, rather like the Awodey-Kishida case. I wonder if any other such (co)monads arising from base change along units and counits of the table and adjunctions give interesting modalities.

• CommentRowNumber66.
• CommentAuthorMike Shulman
• CommentTimeJun 14th 2016

There are some comments in Remark 7.7 of my realcohesion paper about how spatial type theory is related to the Awodey et. al. semantics for modal logic, in case that is helpful.

• CommentRowNumber67.
• CommentAuthorDavid_Corfield
• CommentTimeJun 27th 2016
• (edited Jun 27th 2016)

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.

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?

• CommentRowNumber68.
• CommentAuthorDavid_Corfield
• CommentTimeJun 27th 2016

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.

• CommentRowNumber69.
• CommentAuthorUrs
• CommentTimeJun 27th 2016

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.

• CommentRowNumber70.
• CommentAuthorDavid_Corfield
• CommentTimeJun 27th 2016

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

• CommentRowNumber71.
• CommentAuthorUrs
• CommentTimeJun 27th 2016
• (edited Jun 27th 2016)

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

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

2. 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.

• CommentRowNumber72.
• CommentAuthorDavid_Corfield
• CommentTimeJun 27th 2016

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?

• CommentRowNumber73.
• CommentAuthorUrs
• CommentTimeJun 28th 2016
• (edited Jun 28th 2016)

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} \,.$
• CommentRowNumber74.
• CommentAuthorDavid_Corfield
• CommentTimeJun 28th 2016
• (edited Jun 28th 2016)

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 ionad is 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.]

• CommentRowNumber75.
• CommentAuthorDavid_Corfield
• CommentTimeJun 28th 2016

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).$
• CommentRowNumber76.
• CommentAuthorUrs
• CommentTimeJun 28th 2016

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

• CommentRowNumber77.
• CommentAuthorDavid_Corfield
• CommentTimeJun 28th 2016

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.

• CommentRowNumber78.
• CommentAuthorUrs
• CommentTimeJun 28th 2016

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.

• CommentRowNumber79.
• CommentAuthorDavid_Corfield
• CommentTimeJun 28th 2016

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.

• CommentRowNumber80.
• CommentAuthorDavid_Corfield
• CommentTimeJun 29th 2016
• (edited Jun 29th 2016)

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.

• CommentRowNumber81.
• CommentAuthorUrs
• CommentTimeJun 29th 2016

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?

• CommentRowNumber82.
• CommentAuthorDavid_Corfield
• CommentTimeJun 29th 2016

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.

• CommentRowNumber83.
• CommentAuthorDavid_Corfield
• CommentTimeAug 22nd 2018

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