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.
added to modality a minimum of pointers to the meaning in philosophy (Kant).
There’s a question here of what we want such entries to do. Kant and Hegel just wouldn’t appear on a modern Anglophone encyclopedia page on modality, e.g., SEP. If I’ve been slow to fill in philosophy entries, it’s from a sense of how little is established in the right form for reasonably well-rounded entries.
I think it best not to aim for an impossible neutral POV, and so we should cherry pick whatever fits with the nPOV.
I know there are different styles of mathematics, but the variation within philosophy is extreme. Take a look at who’s invited you to Paris, Catren. Move him a few miles north over the English Channel, and if he tried to speak like this in most philosophy departments, people would rush for the door.
I see.
But isn’t it right that the terminology in modal logic is explicitly following/inspired by Kant’s original terminology? Interpreting S4 modal logic as being about necessity/possibility seems to have little intrinsic justification and instead seems to be all inspired by Kant. No?
Concerning the link you give, you may have to help me and say more explicitly what style is being violted here.
Of course, Kant should appear in any history of modal logic, but a fuller story of modal logic would certainly go back to the Greeks. The Mediaeval period was active too (here). Descartes and Leibniz would have to be mentioned.
What specifically do you think Kant did to give him such a prominent place? There’s a good short summary of his ideas here.
For what Anglophones take as modal logic today you would perhaps start with C. I. Lewis, as here.
Regarding the link, the style would be considered too poetic, a flowery combinations of words rather than careful argument. Also the choice of philosophers to refer to would be off-putting to many here (Berman, Blanchot, Deleuze and Guattari, Derrida, Gentile, Hegel, Heidegger, Lacan, Benjamin).
The English department at Cambridge wanted to award an honorary doctorate to Derrida, but the philosophy department blocked it, wikipedia.
Philosophy really is a very odd subject. We have an eminent Oxford don who comes to speak to us for 6 weeks through the year. During the last talk he claimed 99% of (analytic) philosophers of language are going about things in completely the wrong way.
Okay, so what I did at modality is certainly not meant to be comprehensive. All I did was feel that the entry needs to say something about modality in philosophy, looked around and saw those S4 modalities named in Kant’s categories. So I entered that. Seems to me adding this to the entry is better than not adding it, it increases the value only by but at least it does increase it by a positive value, I thought. If not, let’s edit it.
Concerning those debates you mention: I clearly have an outsider perception here, to me it seems to be part and parcel of philosophy as a whole that there is no definite way, as there is in maths, to find agreement or to tell the difference between flowery words and careful arguments. I can see that some texts have more of a feel of careful argument to them, but with all terms under discussion usually lacking a precise definition, a careful-looking argument can even be more deceptive than those flowery words, sometimes. For instance, back then those alleged proofs of the “existence of God” were considered careful arguments, certainly they tried to immitate the style. But that’s deception. Here for instance flowery Hegelian prose seems to me to capture more of the essence.
I’m not objecting to the additions. If I was doing anything in #2, I was explaining why I’ve done so little for the philosophy entries. Actually it’s refreshing to watch an outsider pick up whatever pieces interest them. I’m fond of the idea of philosophy as a storehouse of interesting, suggestive ideas, and agree with your second paragraph. Case in point about the storehouse, most people today wouldn’t have being-nothing as modalities.
Perhaps when we’re through with Hegel, we can give Charles Peirce a go. After all, it was he who, from a distance of over a century, provided Mike with his diagrams for indexed monoidal categories. Also he has vast amounts to say about modality, including ideas for graphs I mentioned in response to an interesting idea by Neel Krishnaswami of modalities as internalised judgements.
In the process of looking about just now for Peirce’s views on Hegel (an interesting ambivalence), I found another attack on Hegel, this time by Reichenbach (Hegel’s system is the poor construction of a fanatic…)
Perhaps when we’re through with Hegel, we can give Charles Peirce a go.
Maybe, but I need to warn you: I am hopelessly selfish and utilitaristic in my interest in philosophy. I got excited by Hegel because I obtained actual insight for my research from reading him (thanks to your prodding!) , and since I kept having the feeling of a related soul being after something un-nameable that I feel I am searching, too.
Right now I feel that next I need to get this kind of inspiration on topics of a more linear-logic and quantum nature. The discussion we started having at quantum logic needs more thinking. It seems amazing to me that nobody should have put 1+1 together as Ambramsky-Duncan did (e.g. here). This needs to be followed up on. I am afraid that this will occupy my non-formal-maths cycles next.
Maybe there’s no need to move on from Hegel then :)
I claim that reading quantum physics through Hegel and vice versa is very productive. (Zizek)
There’s another character who is hero or charlatan depending on your POV.
Hm, interesting. I had no idea that somebody like him would take interest in metaphysics.
He writes:
I claim that what is happening, for example, in quantum physics in the last 100 of years – these things which are so daring, incredible, that we cannot include into our conscious view of reality – that Hegel’s philosophy, with all it’s dialectical paradoxes, can be of some help here
Now, I suspect what he has in mind is just the rough idea of something like “wave-particle duality” as an instance of “Heglian opposites”.
While I don’t see this directly, with our Lawverian formalization of Hegel we can go now and prove or disprove claims like this. And here is one thing we can say:
the upshot of Type-semantics for quantization is that in formalized Hegelian metaphysics there is induced a natural notion of quantization via integral transforms. Wave-particle duality may be thought of as being formalized by one instance of such a transform (Fourier duality). And so that does formally connect Hegelian dialectics with quantum duality.
Of course this way it comes out a bit more nuanced than what might be suggested in the above: we don’t get “wave particle” as an explicit adjoint modality. But from some adjoint modalities we do get something else that reflects wave/particle duality.
I have added that quote at the end of Hegel – Percetion. Fun.
Zizek has a chapter The ontology of quantum physics in Less Than Nothing: Hegel and the Shadow of Dialectical Materialism.
Thanks for the pointer!
At least he does try to follow modern physics, talks about quantum mechanics at all, has heard of strings and branes, has heard of the would-be philosophy debates expressed in popular books such as Hawking’s, has tried to form an idea and an opinion, has an open mind. That’s more than can be said of many possibly otherwise deeper thinkers.
After all, it was he who, from a distance of over a century, provided Mike with his diagrams for indexed monoidal categories.
After a somewhat creative reading of Peirce. :-)
Oh yes, right, we absolutely shouldn’t forget your role.
Perhaps it’s not easy to say, but how much ’work’ did it need to turn the existential graphs into category theory?
At this remove in time it’s a little hard to say how hard it was, or what my state of knowledge was when Gerry Brady and I began the project. I think I knew about hyperdoctrines or at least hyperdoctrinal ideas, and I certainly knew about string diagram calculus, linear logic, operads, and some rewriting theory, and my memory is that it wasn’t too hard to draw a connection between the existential graphs and string diagrams, and how to use the other stuff mentioned to help put it together formally. Probably what happened is that Gerry had seen me discussing string diagrams in the early days of the U. Chicago category seminar, and they reminded her of the existential graphs (which she had known from her detailed historical research on logic from that era; cf. her book on Peirce, Schroeder, Lowenheim, and Skolem). I do have a clear memory that she took me aside one day after seminar to ask me if I thought there could be a connection between string diagrams and existential graphs (which I hadn’t known about before she told me about them).
I don’t recall how hard were the specific technical problems (e.g., the material you brought to Mike’s attention at the Café when he was blogging about monoidal fibrations), but I’ll say that I always had a nagging feeling, which persists to this day, that the existential graphs were being “shoehorned” into category theory, in the sense that existential graphs really don’t have a sense of directionality (domain and codomain, past and future) that string diagrams and Feynman-type spacetime diagrams do. Really the existential graphs are composed more in cyclic or modular operad style, reminiscent of Sean Carmody’s thesis on cobordism categories. My thoughts and memories are somewhat vague as I write now – I’d have to think harder about this – but the idea of taking traces should play a bigger role in the formalization than was made manifest in what Gerry and I did.
Since modality is being brought up here, I’ll say that I slightly resisted the idea (pushed by C.I. Lewis) that Peirce’s Gamma was all about modal logic. Or rather (since it is manifestly about modal logic!) that thinking along Lewis’s lines wasn’t necessarily the most clarifying, that really Peirce was anticipating higher-order logic and ideas of topos theory or power allegories, etc. (extending Beta which was just first-order logic with equality). Of course we know now, through work that passes through Kripke, Lawvere, and Awodey-Kishida, etc., of the tight interconnections between modal logic and sheaf theory – but I definitely thought at the time that aspects of higher-order logic hidden in his research on Gamma had been underplayed. The trouble, though, is that I could again be shoehorning his obscure thoughts into stuff I happen to know – some of the historical antecedents are sketchy to say the least, and based on just a tiny bit of archival material that I’ve seen (in Peirce’s own handwriting!) that is extremely hard to find – not in his collected works which, by the way, Lewis had a major hand in culling. So these personal readings would be extremely hard to justify, based on the available evidence.
(Edit: this “shoehorning” was in part what I was slyly suggesting when I used the word “creative” – it wasn’t just flat-out self-promotion on my part. (-: )
This feeling of “shoehorning” more generally seems to apply to compact closed gizmos in general: there really isn’t a directionality, but we impose one in order to use the category-theoretic machinery. Unfortunately, it seems to be quite tricky to come up with a good formalism to study such things without this sort of shoehorning.
Thanks, Todd, for those reflections. About directionality, I wonder if there were further thoughts on Noah Snyder’s operadic periodic table. He was searching for more natural settings when no directions were present, so looking to the right side of his table.
Re modal logic, I said elsewhere that Neel Krishnaswami’s remark struck me as having a Peircean flavour.
With the definition of modality in section 7.7 of the HoTT book, and now in A Generalized Blakers-Massey Theorem
a factorization system (L,R) on the category of spaces with the additional property that the left class L is stable under base change. We refer to a factorization system satsifying this condition as a modality, a term originating in the literature on type theory [Uni13, Section 7.7],
is there something settled to add to modality?
We could certainly add that definition, as long as we emphasize that “modality” is only a shorthand for “idempotent monadic modality” when those are the only ones of interest.
I made some edits and links to our paper Modalities in homotopy type theory in modality, modal type theory, modal homotopy type theory, reflective subuniverse, idempotent+(infinity%2C1)-monad, idempotent monad. There seems to be a bit of duplication in those pages.
From Modalities in homotopy type theory
Independent type theory, such as homotopy type theory, where propositions are regarded as certain types, it is natural to extend the notion of modality to a unary operation on types.
Does anyone know who first had the idea of applying modalities to sets, etc.? As I said back here
Despite the enormous amount of attention given over to modal logic by philosophers, I’m unaware of any mention of the idea that modal operators could apply to anything other than propositions.
I would imagine the step went from making ordinary applications of modal operators to propositions, and then taking these latter as not just ’mere’, i.e., potentially having multiple distinct proofs. Is that right?
We call it a “fracture theorem” since the pullback squares appear formally analogous to the fracture squares in the classical theory of localization and completion at primes, though we do not know of a precise relationship.
With all that Urs has done at fracture theorem, differential cohomology diagram, differential cohesion and idelic structure, is this relationship really not known?
Re: #22, perhaps we should have been more explicit. There is obviously a close relationship, but the reason I don’t see a precise relationship (by which I mean a theorem that can be proven saying that one thing is an instance of something else) is that the fracture theorem in the paper is about lex modalities on toposes and applies to all types. The most classical fracture theorem is about reflective subuniverses (that are not even modalities) on the topos of -groupoids but applies only to a restricted subclass of objects (e.g. nilpotent ones). One can state it as a theorem about spectra instead to remove the nilpotence condition, but spectra are no longer an -topos. Probably there is a version that applies in the -topos of parametrized spectra, and maybe just maybe in that world the relevant subuniverses actually turn out to be lex modalities, so that our theorem would actually apply — but I have not seen such a version written out anywhere, and a quick glance just now at fracture theorem didn’t turn it up either. Did I just miss it?
There was talk here about exactness not holding in general for hexagons, even in the case of parametrized spectra. Hmm, but is that exactness (a bunch of interlocking fiber sequences) more demanding than you need?
Conversely, I had no idea that Artin gluing is internally a fracturing, according to section 3.4 of Modalities in HoTT. That’s beautiful.
Regarding the paragraph on p. 5:
Viewing accessible lex modalities as subtoposes,… reduce the problem of finding univalent internal languages for ∞-toposes to that of finding them for presheaf ∞-toposes.
Does this mean that given an interpreation of in a model category for some -topos (say the injective model structure on simplicial presheaves over an elegant Reedy category) that also all of its left exact Bousfield localizations will interpret ?
Mike was pointing in this direction four years ago in his The Propositional Fracture Theorem. Did anything come of
This suggests that we might regard internal gluing as a “generalized sort of case analysis”… I have no idea whether this sort of generalized case analysis is useful for anything. I kind of suspect it isn’t, since otherwise people would have discovered it, and be using it, and I would have heard about it?
Also there is the link to fracture theorems, such as the one that applies
… to any space (with technical conditions), yielding a pullback square
where denotes localization at .
Clearly, there is a formal resemblance to the pullback square involved in the gluing theorem. At this point I feel like I should be saying something about .
Did anything come of
No, not yet, but I haven’t lost hope. (-:
Does this mean that given an interpreation of in a model category for some -topos (say the injective model structure on simplicial presheaves over an elegant Reedy category) that also all of its left exact Bousfield localizations will interpret ?
Sort of; you need enough ambient strict universes that are closed under the localization in a strict sense. I don’t know how to ensure that. Probably we should be more clear about that in the paper.
Presumbably the thought was tied to this at fracture theorem
the arithmetic fracture square of prop. 2.1 says that the curve has a cover whose patches are the complement of the curve by some points, and the formal disks around these points.
These comments are very helpful, by the way; I am adding more detailed remarks to the paper about all of them.
Can the gluing used for syntactic categories (as in Scones, Logical Relations, and Parametricity) be seen in a modal fracturing light?
Hmm, scones (at least here) seem to be linking and . But I really should be doing something else.
Inside of any glued topes there are open and closed modalities that fracture it into the two toposes that were glued. I don’t know whether this produces useful insights when applied in a syntactic scone.
I am going to spell out some elementary basics regarding (co)reflective subcategories and (co)modal/(co)localization endofunctors, on the Lab, lecture note style. Which entry would sensibly host the following definition? I am inclined to have this under “modality” in a section “In category theory” with the understanding that more refined definition exists and will follow. But let me know if anyone has strong opinions about this.
Consider
an endofunctor
whose full essential image we denote by
for all objects , to be called the unit morphism;
such that:
for every object in the essential image of , every morphism into factors uniquely through the unit
Dually:
a comodal operator on is
an endofunctor
whose full essential image we denote by
for all objects , to be called the counit morphism;
such that:
for every object in the essential image of , every morphism out of factors uniquely through the counit
We had a learned discussion about ’comodality’ back here, and I thought the consensus was opposed to it and in favour of ’comonadic modality’.
Could better naming be suggested by the Shulman-Licata-Riley approach? Modal logic is the logic associated to modes, which feature in a 2-category. But has this settled yet?
In Adjoint Logic with a 2-Category of Modes: A pseudofunctor from a 2-category of modes, to , the 2-category of categories, adjunctions, and conjugate natural transformations.
We don’t seem to have an nLab page on such a 2-category.
Then in Mike’s HoTTEST talk, it’s . Why these choices?
So that’s a general process, right, where a 2-category is sent to the 2-category of adjunctions within it. Reapplying this map, a morphism in the resulting 2-category is an adjoint triple in the original 2-category.
To be specific, the kind of material that, I think, would usefully be spelled out in – or at least linked to from – relevant entries (many of which are lacking any indication of details) is the (basic) stuff written out here.
Terminology may be changed, of course, but let’s not get this debate too much in the way of the content.
Since this is a purely category-theoretic definition, I would put it at reflective subcategory or idempotent monad. A category-theoretic terminology for the functor itself would be “reflector”. In certain contexts this could be called simply a “modality” (e.g. the HoTT Book), but the notion of modality is more general than this, so I would not want to put this forward as if it were the definition on page modality.
Re #34, what exactly is the question you’re asking?
Re #35, yes, there’s an operation on 2-categories. I agree, we should have a page about this.
Yes #34 was rather a muddle, but if there is a question there it’s perhaps about the orientations of the 2-categories, e.g., is the choice of right adjoints in just a convention?
Are there standard names associated with ?
what exactly is the question you’re asking?
The question was in #32:
Which entry would sensibly host the following definition? I am inclined to have this under “modality” in a section “In category theory” with the understanding that more refined definition exists and will follow. But let me know if anyone has strong opinions about this.
I think Mike was wondering what I meant by #34.
Oh, I see, sorry. And only now do I see the reply in #37.
Yes, the choice of right vs left adjoints is a convention. In fact LS and LSR use different conventions.
Maybe would be 2-category of adjunctions? Or just Adj.
Emily Riehl has as the walking adjunction here, saying this comes from Schanuel-Street.
Makes sense. Then is composed of 2-functors .
So , adjoint triples in , is also . I guess that makes a dependent type 2-theory, since these concern maps .
Then is composed of 2-functors .
For some meaning of “composed of”, but it’s not the functor category : its objects are the objects of , and its morphisms are the functors .
Whoops. Will fix.
I guess the “open modality” Ex 1.7 of Modalities in HoTT () is the reader monad for a proposition.
Thanks. Notice that this entry “modality” is a bit of a disambiguation entry, the dedicated page for modal homotopy type theory is modal homotopy type theory. I’ll copy over your addition to there.
For some reason, the \bigcirc on this page is displayed as a filled-in circle in my browser. Does anyone else see that?
Re #52, no not on mine.
52: I also see filled-in circles on mine
1 to 55 of 55