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.
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.
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).
@David I have been quietly increasing (slowly) the coalgebraic related stuff with a view to pushing that link further.
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.
@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.)
My queries are silly ones such as ’What would be the higher dimensional language accepted by a higher dimensional automaton?’
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.
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?
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.
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 . The epistemic logics use multi-equivalence relations for their models. Perhaps n-dimensional situations require relations that are (n+1)-ary.
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.
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?
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.)
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 is the set of worlds, and we have a relation . Now, suppose our frame arises as the transitive closure of . Then a proposition like holds at a world if holds in every world reachable from . Now, the point is that can’t distinguish between two relations and which happen to have the same transitive closure. That is, if and , viewed as the big-step transition systems induced by the closure operation, are bisimilar, then they will prove the same formulas.
@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! :-)
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.
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!
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 , corresponding to the relation on set of worlds , we have a , which to every world in category of worlds gives the functor of accessibility. Seems to be a kind of 2-coalgebra.
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.
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).
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’).
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.
I forgot to mention bounded morphisms that are clearly fibrations in all but name.
Digging out a student essay, I have the claim that
( 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.
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.
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.
@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.)
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 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 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 reflexive relations on it.
(Edit: When proving that I was thinking, how does one do all this in a more constructive or intuitionistic setting? )
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.
@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.
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!)
@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.
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.
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.
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?))
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?
Of course, the first recorded use of the symbol 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.
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, , and either works via a frame , or else via a map which may be the interior operation on a subset.
We ought to play the same game with and .
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: . Then it could matter which way you get from one world to another. In the propositional case, take and , where we can access the second from the first but not the other way around. Then we have true at if holds at both worlds.
Imagine now there are two ways of getting from to . 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 , then we would have the situation where holds at 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’.
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.
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.
In the propositional case, you have two pictures for the accessibility relation:
Either, a frame (relation) , or, an operation on subsets of , .
If 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, . That leaves me wondering about the corresponding general frames . Is there a slick arrow-theoretic way to characterise the passage from the relation to the operation on subsets of , ?
@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.
I was just wondering how to analogise the mechanism from frame to topology, to one between some kind of and ionads. Trying to understand Garner’s paper, part of the story is that given a certain kind of , one can place a category structure, , on the set , such that . Then the interior operation takes to .
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.
So what’s the idea of it, in a few plain sentences? How about this:
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.
That looks reasonable to me, but I’m not really a modal-logician as such.
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?)
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.
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.
Made one or two changes, but had less time than I thought, so will have to come back later.
I have not checked who made what changes, but I like the way the ideas section is shaping up.
I am gradually discovering lots of well hidden 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.
I have made a start with creating a subsection Modal logic – Examples.
Probably there are more entries that could go there. Who knows about them. Tim?
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.:-))
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…
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.
In case this helps for the semantics vs. syntax discussion, there is an entry on the Lindenbaum-Tarski algebra of a normal modal logic.
I just came on a paper by Mai Gehrke here, that may be of interest.
I have added relevant material that people have been mentioning on the 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.
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.
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.
Split off first-order modal logic, but no time to do anything substantial.
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.
Link to the paper of Goldblatt at modal logic does not work.
It does now. There was an http:// missing.
have added to modal logic the reference
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.
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 of sets indexed over a set to the topos of sheaves over a topological space induced by the (continuous) identity map . The modal operator is interpreted by the interior operation that the comonad induces on the Boolean algebra of subsets of ,
it sounds reminiscent of the 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, and , in Urs’s cohesion - table:
and
What could we do with the counit of the comodality ?
So we have again acting on , 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.
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.
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, , 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 ?
Again four (co)monads from the composites. Can we name any of them?
It would probably be better for the soul to work this out myself.
So is a forgetting of the flatness of a connection.
Then provides a pullback, so is a general version of the dR-flat modality.
So 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 -construction.
The must be a universal way to flatten a connection on an -bundle.
You mean: to pick trivial underlying -groupoid -bundles.
Consider first pointed connected coefficients, hence of the form . Then the homotopy pullback
has the following interpretation: its generalized elements consist of
a flat connection with underlying bundle ;
an equivalence .
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 to any , then 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 . You may choose to pick all of these connected components and all of the transformations between them, and then consider the homotopy pullback in
Clearly this has some relation to . I suppose if one picks one representative points in each connected component of and hence pulls back along some , then one obtains the “right” definition of for groupoid-principal connections.
Right now I am not sure what it means to retain all the higher homotopy information of the in the bottom left corner.
But I agree that this looks like a sensibel perspective from which to view in generality.
Well I just meant that there’s some process which takes us from some bundle to some other bundle . Wouldn’t we call that a ’flattening’.
Anyway, I was with you so far, but then why do you have in both corners of that square?
then why do you have in both corners of that square?
I thought that’s what you were suggesting to look at. The operation in your #67 above is the operation that sends any to the pullback
I thought your point in #68 had been to observe that then the -operation becomes sort of a special case of the possibility-like modality , via
Oh, I see. I though we were just working out , 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 , but all seems to point to the other way,
An ionad is a set together with a finite limit-preserving comonad on the category
chimes with
In the original expression, we consider the geometric morphism from the topos of sets indexed over a set to the topos of sheaves over a topological space induced by the (continuous) identity map . The modal operator is interpreted by the interior operation that the comonad induces on the Boolean algebra of subsets of .
[EDIT: These are, of course, using the right adjoint to , but still the interest is starting out from the discrete side.]
Just to clarify, my initial thought was that we had a case already of the operation of :
Oh, I see. That’s of course, true, too.
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.
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 of -indexed sets is the slice for any object in the -topos . Now you are asking for finite -limit preserving comonads on such slices. You get one such by base change along any morphism out of .
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.
Well I’d still like to know the ’meanings’ of the comonad, , and monad, , on . 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 ? 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 -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.
Where would it take us then if we declare:
An -ionad is given by an -groupoid, , and a finite -limit preserving comonad, ?
Then we could have:
The -category of opens of an -ionad is the category of -coalgebras.
This would be an -topos.
Presumably there would be no reason to stick to as the base topos.
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?
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 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:
added pointer to:
added pointer to English translation of Becker’s old text:
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:
1 to 90 of 90