On the scale of justification (#34) I think I would be inclined to put that *below* the set theorists expecting there to be a fact of the matter regarding the universe of sets.

Re 36: bizarre! It never would have occurred to me to suppose that “metaphysical necessity” was a meaningful thing.

]]>Is there some connection between linking modalities via

$\Box = \not \diamond \not$and ’classical’ logic? I mean, say you take $\not \not$ as monadic modality $\diamond$. Then

$\Box = \not \diamond \not = \not (\not \not) \not = (\not \not)(\not \not) = \diamond \diamond = \diamond.$So $\diamond$ is also a comonad. So the unit and counit give $P \leftrightarrow \not \not P$.

]]>Yes, to the extent they’re talking about ’metaphysical’ necessity. Of course, we use modal language to describe what we do or don’t know, “It’s possible she’s already arrived”, but sticking with metaphysical necessity, modal realists believe there’s a fact of the matter.

]]>There are philosophers who believe there is an absolute nature of “necessity”, independently of how the word is used in human language?

]]>So there are three groups of people - physicists understanding the universe, mathematicians understanding set theory, philosophers understanding necessity. Which would you say are most justified in expecting there to be a ’fact of the matter’? Perhaps, physicists then philosophers then mathematicians? If you held the (maybe) reasonable theses that there’s a single best description of the universe, but a plurality of good set theories, what would you expect of the philosopher on necessity. Are they more like the mathematician, providing a range of possible logical characterisations that cover what we might take to be the concept of necessity, or more like the physicist, finding out the true nature of necessity?

You certainly find both kinds of philosopher. And then also those who think formalisation is misguided, and that one should look at language in ordinary use.

]]>Re 28, some modern set theorists also seem to think there is a ’fact of the matter’ about the continuum hypothesis which remains to be discovered.

]]>There are some issues here. First, in modal (homotopy) type theory maps $\diamond A \to \square \diamond A$ in general don’t *merely exist* (to adopt that language) but are a choice. So one would have to ask if there are such choices and which further compatibility laws these should possibly satisfy.

Then, I guess another issue is that in modal logic one assumes the relation

$\Box = \not \diamond \not$between the two modal operators. Since now we really need to be talking about both of them, we’d need to lift this to modal type theory at least. But there it’s not clear to me what would usefully replace this. We might just blindly interpret $\not$ as the internal hom into the initial object, but then certainly no pairs of modalities seen in cohesion would satisfy this.

If we ignore this and just take $\diamond$ to be the shape modality and $\Box$ to be then the flat modality, then one has

$\Box \diamond \simeq \diamond$(since $\diamond$ goes to discrete objects and these are the $\Box$-closed objects). So on the one hand a natural map $\diamond A \to \Box \diamond A$ certainly exists, but on the other hand this does not seem to be interesting in this context.

So it seems that a lift of S5 to cohesive (homotopy) type theory is not strictly possible and relaxed variants are not interesting.

Maybe if we just ask more generally for lifts to modal type theory more can be said. Well, I guess people who studied modal type theory must have looked into precisely this question?! But I don’t know.

]]>Which pairs of monadic and comonadic modalities that we know and love from (cohesive) type theory satisfy (5) ◊A→□◊A ?

Is there a set of examples of comonadic modalities to parallel examples 1.3-1.8 in Mike’s notes?

]]>The structure on the collection of possible worlds is one of the least interesting for S5, i.e., just an equivalence relation, so in terms of accessibility from a particular world, one just looks at the class of that world, and says every world is accessible to every other (e.g., here). Obviously there are more interesting structures one might put on the way worlds are related to capture temporal logic, etc.

By the connection to probability theory, are you envisaging a ’possibility’ map $[0, 1] \to \{True, False\}$, where $0$ is sent to False, and True otherwise, which then induces a map from probabilities of outcomes to possibilities of outcomes? So a map from the Giry monad to the possibility monad.

Hmm, isn’t (5) ◊A→□◊A problematic as a projection from probabilities? Damn, I’ve no time for this!

]]>David,

thanks, yes, so this is what I was complaining about in #24. But I take that back. While I still think this is a complain-worthy attitude, I now understand (which I had missed before, sorry, I never really looked into classical modal logic) that modal semantics provides a formal interpretation of “possible” which is really the same notion of “possible” as in probability theory and hence entirely respectable. I think.

Also in probability theory there are people arguing about what “probability really means” by which they mean some physical flavour of meaning. But this I don’t worry about. It is sufficient to have a set and a formal theory about measures on this set. In modal logic that set is the set $W$ “of worlds”. But whether we think of these as “worlds” or not, is not important. What is important is, as far as I can see, that S5 modal logic is provably precisely that extension of propositional logic where the diamond operator has the interpretation “true over some points of this set”.

I didn’t appreciate this before. (And is it just my fault? One sees people all over the place advertize S4 as the logic of necessity, but it is S5 only which really is! People should advertize S5. )

This is good. If I weren’t absorbed with other things, I would highlight this in some $n$Lab entry to save other people like me from similarly missing this simple fact for so long.

]]>Some philosophers act as though they’re doing something much more akin to physicists arguing about how the universe is, that they have some way to determine what can be said modally. For example, one prominent English philosopher claims that finding that $\Box P$ entails $\Box \Box P$ was one of philosophy’s finest discoveries.

Some even believe in the possible worlds semantics. That there is a close possible world where my counterpart eats an egg for breakfast is what makes true the statement “I might have had an egg for breakfast.”

]]>Or Euclid’s fifth axiom. To name an example that historically saw the same kind of arguments about its absolute truth, which today has been fully recognized as just an arbitrary axiom.

]]>Heh, #23 could also apply to mathematicians arguing about whether the axiom of choice or the continuum hypothesis are true.

]]>Ah, I take that back. I just read through *SEP - Modal Logic* for the first time, and learned for the first time of the result that with reasonable assumptions one can prove that “necessity”/”possibility” is indeed accurately axiomatized… but it is S5 that does so (which has a monad and a comonad interacting in some way), and not S4 (which just has a comonad). (I am referring to the point where the SEP entry talks about “5-validity”).

Something I’d certainly want in my space of possible worlds is some holonomy, so I could transport some collection of objects in this world through their counterparts along a path through possible worlds and back to this world, thereby generating a permutation.

What precisely do you mean by “world”, by “possible” and by “possible world”?

Isn’t that the big problem which leads to the odd situation which you highlight so well: that one is operating with these English words with them having either no precise meaning or else having been given a precise meaning that however falls radically short of capturing the more vague but much richer meaning in English which their uttering invokes?

For instance what in the above discussion is it about $\diamond$ that makes people think that it accurately reflects a nontrivial portion of the meaning of “possible”?

When I say that “I take $\diamond$ to be the shape modality”, then this means that I consider it equipped with a good bit of extra property (namely being the left part in an adjoint triple of higher modalities and preserving finite products). And I claim to have checked that for any $\diamond$ which does satisfy all these extra properties, interpreting it indeed as producing shape/fundamental $\infty$-groupoids is consistent in that it makes a whole bunch of statements involving $\diamond$ have a consistent and nontrivial such interpretation for a whole bunch of aspects of the meaning of shape/fundamental $\infty$-groupoid.

Is there some analog of this for “possibility modalities”? I suspect that people are saying “possibility modality” to something whose axioms may be necessary to support that interpretation, but which are far from sufficient for it.

In particular if we start saying things like “world” in conjunction with “possible” and start alluding to concepts of physics. I mean, I have voiced surprise about how many aspects of physics can be captured by the simple axioms of cohesion, but it seems to me some of those people whose ideas we talk about assume that with much fewer axioms even way more physics is faithfully captured. This must be a delusion, and to the extent that it is made implicitly, it must be a source of great confusion.

]]>Re #22, that would open things up nicely.

It’s an odd thing this business. Philosophers have these passionate debates about whether we should quantify over all actual objects in the universe or all possible objects, about whether there are unique counterparts or not to any object in a given neighbouring possible world, whether a transworld object has its being fully in the actual world, etc., as though there’s a fact of the matter about how to resolve them.

Strangely, though, they seem to be dealing with some impoverished shadows of interesting mathematical structures, which ought to provide them with a much richer set of tools to continue their arguments, but which could also ought to lead them to think there is no way to determine whether to impose this or that condition on, say, the quasitopos of concrete sheaves on merely metaphysical grounds.

Something I’d certainly want in my space of possible worlds is some holonomy, so I could transport some collection of objects in this world through their counterparts along a path through possible worlds and back to this world, thereby generating a permutation. Philosophy has been rather boring in requiring accessibility relations between worlds to be merely relational.

]]>Much will depend on whether we go sheaf theoretic, and expect individuals in a world to have unique counterparts in neighbouring worlds, or better path-dependent unique counterparts.

If you want individuals to have non-unique counterparts in a neighboring world, then you could replace the morphism $W_1\to W_2$ in a (pre)sheaf model with a span $W_1 \leftarrow R \to W_2$, with $R$ the witnesses of “counterpartness” between pairs of individuals in $W_1$ and $W_2$. By passing to a quasitopos of concrete sheaves, you could moreover probably enforce that $R \to W_1 \times W_2$ is monic, so that $R$ really is a mere relation (rather than containing multiple witnesses of counterpartness for the same two individuals).

]]>Yes.

Oh, I see, I used the term “converse Barcan formula” the wrong way around. Should have paid better attention.

]]>The remark above was

$\left(X \stackrel{\simeq}{\to} \diamond X\right) \;\;\;\Rightarrow \;\;\; \left( \underset{X}{\sum} \diamond_X \simeq \diamond \underset{X}{\sum} \right) \,.$Doesn’t this say that when $X$ is $\diamond$-closed, both the Barcan and converse Barcan formulas hold, since there is an equivalence of types?

The converse Barcan formula is holding for this modality $\Diamond$, since there is a natural map

$\underset{X}{\sum} \diamond_X E \to \diamond \underset{X}{\sum} E.$But the forward Barcan formula holds only for special $X$.

]]>That sounds right to me.

And so in this language my above remark that converse Barcan applies when $X$ is $\diamond$-closed becomes the evident statement:

If all possible teams are actual teams then every possibly player is a possible player of an actual team.

I’d say.

]]>One quick thought. So I could instantiate

$\array{ \underset{X}{\sum}E \\ & \searrow \\ & & \underset{X}{\sum} \diamond_X E &\to& \diamond \underset{X}{\sum} E \\ && \downarrow &pb& \downarrow \\ && X &\to& \diamond X } \,,$with something like

$\array{ players\, of\, actual\, teams \\ & \searrow \\ & & possible\, players\, of\, actual\, teams &\to& possible\, players\, of\, possible\, teams \\ && \downarrow &pb& \downarrow \\ && teams &\to& possible\, teams } \,,$I wonder if that top right entry can be formulated differently

]]>possible players of possible teams = possible (players of teams)?

I’ll try to give some context later today. You should see my Inbox. Any consideration that we might want to do some research has been lost.

But I did overnight have some small inkling of an idea that being allowed to apply modalities to types allows quite a few distinctions that are missing for standard philosophy. Since they never went typed, they’re left wondering what to quantify over in first-order modal logic, and so end with a choice between all actual things or all possible things. But we have such types as:

- players of actual teams
- possible players of actual teams
- players of possible teams
- possible players of possible teams

Much will depend on whether we go sheaf theoretic, and expect individuals in a world to have unique counterparts in neighbouring worlds, or better path-dependent unique counterparts.

Back to admin!

]]>Thanks for the quote.

Hm, just as in our last discussion with a philosopher of physics here, I am somewhat struck by the apparent intent to behave entirely as if classical mechanics was never superceded by quantum physics. In view of the latter, what seems *counterlegal*, to borrow that term, is not the variation in a space of non-classical trajectories, but the counterfactual suggestion that such non-classical trajectories don’t have physical reality.

I don’t have an overview of what is happening in philosophy of physics, but these two examples that I have seen lately remind me of what you used to say about the mainstream in the philosophy of mathematics: that the most important advances in the last century are being ignored.

(Maybe I am being unfair here, having seen just the above quote…)

]]>