Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 10th 2013

    Is there some thought with modal type theory to think about its version of the Barcan formula

    ? \Diamond \exists \to \exists \Diamond?

    For example, we could compare

    x:XA(x) \diamond \sum_{x \colon X} A(x)

    and

    x:XA(x). \sum_{x \colon X} \Diamond A(x).

    If \Diamond were truncation to Prop, the former is a further projection of the latter, suggesting converse Barcan holds.

    But it would be nice if I could illustrate things using the language of possibility. If the dependent type represents players for a team, we could talk of a possible team player and some team’s possible player, the latter being more informative.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeMar 11th 2013

    I agree with the last sentence. In xA(x)\diamond \sum_x A(x), the xx is only possible; while in xA(x)\sum_x \Diamond A(x), the xx is actual. I've not heard of the Barcan formula, but I'd be inclined to think that its converse is more plausible, whether or not one is thinking of dependent types.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 11th 2013

    You can see from this search that the Barcan formula (sometimes taken as ∀x□A(x)→□∀xA(x)) has generated plenty of discussion in analytic philosophy. Here is a good indication of the kinds of treatment it receives.

    But I’m interested in selling the idea that predicate logic is a projection of dependent type theory, so would like to explore what happens when we add modality. There seems to be a difference between

    He could be a League 1 player,

    and

    There’s a League 1 team he could play for.

    Barcan doesn’t hold since I might have someone currently playing for a League 2 side. In a close possible world that team might have been in League 1 and the player still play for them. On the other hand, there may be some reason the player is strictly not allowed to play for current League 1 sides, so that even in near worlds he couldn’t play for them.

    But then maybe converse Barcan is problematic as well if I could interpret the latter statement as, there’s a team which happens to be in League 1, but in a close possible world it’s in League 2 and the player could play for it there. Perhaps the player is banned from League 1 in all worlds. I could say “He could play for X”, where X is in League 1, but likely to be relegated.

    The semantics for modal dependent type theory should be interesting. Already at the level of predicate logic, we have tuples of individuals fibred above the worlds they inhabit. With dependent type theory, we’ll have fibring within the fibres.

    • CommentRowNumber4.
    • CommentAuthorjim_stasheff
    • CommentTimeMar 11th 2013
    where's the homotopy?
    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 11th 2013

    where’s the homotopy?

    I’ve only taken things to the level of 0-types, i.e., sets. So how might we take things up to 1-types, say, the road system of a country?

    Hmm, let’s have A(x)A(x) be the round trips I can take from x:Cityx: City. Then we could talk of possible round trips in the country and some city’s possible round trips.

    Not too exciting perhaps. I wonder if there’s a more interesting version with a space fibred over another. Mike mentioned in one of his papers that trunction of a type to any level is a modal operator. Let’s take 0-truncation to a type’s path connected components.

    Say, the dependent type has x:Xx:X, with XX a circle, and all A(x)A(x) also equivalent to a circle. So the dependent sum is a torus fibred over a circle. One side of the Barcan formula is equivalent to a point, while the other is equivalent to a circle.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2013

    But then maybe converse Barcan is problematic as well if I could interpret the latter statement as, there’s a team which happens to be in League 1, but in a close possible world it’s in League 2 and the player could play for it there.

    In that case, I would argue that “There’s a League 1 team he could play for” is not true, because in that close possible world the team in question is not in League 1. Switching to a nearby world when hitting the possibility modality shouldn’t allow you to break validity of the current context. That’s how it works in a presheaf model, for instance: in order for it to be true that “X is a League 1 team” then it must remain true at all later worlds.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 11th 2013

    That probably makes sense linguistically too. If we’re doing this in temporal logic, we would probably say

    There’s a team that’s currently in League 1 he might play for in the future,

    with an implication that currently implies possibly not always.

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 12th 2013

    Thinking of the other formulation of Barcan

    ∀x□A(x)→□∀xA(x),

    and moving up to dependent product types, if we take the modality to be the flat modality, we could compare sections of a bundle with fibres made discrete, and a discretised space of sections. Is that right that the latter injects into the former?

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeMar 12th 2013
    • (edited Mar 12th 2013)

    Sorry, I wasn’t paying attention.

    Let me catch up by going back to the original Barcan formula in your message #1, and eventually think of \diamond as the shape modality, dually.

    So first of all, that map

    XX X \diamond \underset{X}{\sum} \to \underset{X}{\sum} \diamond_X

    there, which one is it? For a dependent type x:XE(x)x : X \vdash E(x) and interpreted in the categorical semantics of a cohesive \infty-topos :HH\diamond : \mathbf{H} \to \mathbf{H} we have the maps in

    XE X XE XE pb X X, \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 } \,,

    induced from the naturality of the \diamond-unit applied to the bundle E:XEXE : \underset{X}{\sum}E \to X.

    (Sorry if I am being stupid here, I am kind of absorbed by something else right now.)

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 12th 2013

    Right. So all evidence is pointing to the Barcan formula being invalid and the converse Barcan formula being valid.

    Does this cast light on philosophical discussion of the Barcan formula? So Ruth Barcan proposed as an axiom

    If it is possible that something is F, then something is such that it is possible that it is F.

    Objections were raised for it by reading ‘F’ as meaning “non-identical with every actual object”. Given we disapprove of the Barcan formula, we should not mind this objection.

    What of converse Barcan

    If something is such that it is possible that it is F, then it is possible that something is F?

    Some commentary here says

    The ontology of non-actual possible objects is an integral part of the possibilist view that quantifiers in quantified modal logic range over all possible objects, non-actual as well as actual. This possibilist view validates the Converse Barcan Formula. If we read ‘F’ as meaning “does not exist”, the Converse Barcan Formula says that if something x is such that it is possible that x does not exist, then it is possible that something does not exist. The antecedent is plausibly true, for any one of us, actual people, could have failed to exist. But if so, the consequent is true as well, assuming the truth of the Converse Barcan Formula. But on actualist representationism, no possible world contains a representation which says that something does not exist, for it is contradictory provided that ‘something’ means “some existing thing”. So if the consequent is to be true on actualist representationism, ‘something’ should not mean “some existing thing” but rather should mean “some thing, irrespective of whether it exists”. That is, the existential quantifier in the consequent needs to have a free range independently of the possibility operator in whose scope it occurs, which is hard to fathom on actualist representationism but which the possibilist view allows. The consequent does not even appear to be threatened with contradiction if we assume the possibilist view and let the existential quantifier range over all possible objects, including non-actual ones…

    Marcus [i.e., Barcan] herself proposes the substitutional reading of quantification to skirt the need for non-actual possible objects (Marcus 1976), and later suggests combining it with objectual quantification over actual objects (Marcus 1985/86).

    A lot of people work on this kind of question. When I have a moment to think, I’ll see if, believing logic to be a mere truncated shadow of dependent type theory, and converse Barcan holding in the latter, gives us good reason to hold it in modal logic. What does this suggest for actualist and possibilist thinking?

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 12th 2013

    Urs, so in #9, are you relying on anything special about \diamond as a modality other than that it is monadic?

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeMar 12th 2013
    • (edited Mar 12th 2013)

    Hi David,

    sorry for the slow replies. It will be like this for just a bit longer, though…

    Thanks for the details in #10, now I am beginning to get an idea of what people are thinking of in this context. I followed one of your links which led me to a long list of further references. Right now I can’t really look through this. But how about a quick nLab page Barcan formula summarizing the basic idea and why people discuss it? That would be helpful.

    Now on technical matters: in #10 what one needs to assume in order for the symbol X\diamond_X to have the interpretation that one thinks it should have is that \diamond preserves pullback diagrams of the form displayed above. If that is the case then it follows that the left vertical map X XEX\underset{X}{\sum}\diamond_X E \to X is the correct fiberwise \diamond-closure, hence that X\diamond_X is a closure operator on the slice over XX.

    If \diamond is the shape modality of cohesion, then this turns out to be true (it preserves these pullbacks) but for non-trivial reasons (as far as I can see). To be precise, I had proved this to be true if there is an infinity-cohesive site of definition and using an argument once kindly provided by Mike Shulman. But now with Mike’s general internal formulation of cohesion I suppose it follows more generally. (Need to think about that, I realize…)

    For diamond the shape modality, the X\diamond_X-closure is “Galois-ification”, it sends an arbitrary bundle over XX to one that is \infty-Galois over it (hence is a locally constant \infty-stack over it).

    There is another related example: if we have differential cohesion then there is also the infinitesimal shape modality. This is now the middle piece in an adjoint triple of modalities (by the “cohesive I Ging” :-) and hence preserves the above pullbacks easily. Now it turns out that the X\diamond_X-closed types/objects dependent over XX can be interpreted as all the \infty-stacks over XX, with respect to a certain canonical étale-type of Grothendieck topology on XX. In particular the subcategory of the slice on the X\diamond_X-closed bundles/dependent types is itself again an \infty-topos.

    (We talked about that a while back in the context of formalizing what it means to be a “physical theory”. In that context I pointed out that these X\diamond_X-closed slices give a way of formalizing variational calculus and Euler-Lagrange equations of motion in differential cohesion.)

    Finally a remark on the issue of “converse Barcan formula”: one thing that the above pullback diagram immediately tells us is that if the base object/type XX happens to be \diamond-closed, then there is a natural equivalence

    (XX)(X XX). \left(X \stackrel{\simeq}{\to} \diamond X\right) \;\;\;\Rightarrow \;\;\; \left( \underset{X}{\sum} \diamond_X \simeq \diamond \underset{X}{\sum} \right) \,.

    Which I guess one could call the “converse Barcan formula in (homotopy) type theory”. (?)

    Maybe if you translate that condition into the usual words used in modal logic in the context of Barcan’s formula (“possibly”, “maybe”, etc, I don’t know, haven’t looked at it closely), then you recognize it as something people have considered. (If not, I guess they should!)

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 12th 2013

    Thanks ever so much for this, and no need to worry about your speed. I’m not going to be able to work much on this for a while. If only I didn’t have a thousand other things to do, including my very least favourite task of marking essays. But a few weeks and I’ll be much freer.

    I love how homotopy type theory is bumping up against hardcore analytic philosophy.

    I like the idea of linking the physics to modality. We may very well meet up with Jeremy Butterfield’s work on that (not that with Isham on toposes).

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMar 12th 2013
    • (edited Mar 12th 2013)

    What did Butterfield say about physics and modality? I don’t know!

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 12th 2013

    For example, Some Aspects of Modality in Analytical Mechanics.

    Abstract: This paper discusses some of the modal involvements of analytical mechanics. I first review the elementary aspects of the Lagrangian, Hamiltonian and Hamilton-Jacobi approaches. I then discuss two modal involvements; both are related to David Lewis’ work on modality, especially on counterfactuals. The first is the way Hamilton-Jacobi theory uses ensembles, i.e. sets of possible initial conditions. The structure of this set of ensembles remains to be explored by philosophers. The second is the way the Lagrangian and Hamiltonian approaches’ variational principles state the law of motion by mentioning contralegal dynamical evolutions. This threatens to contravene the principle that any actual truth, in particular an actual law, is made true by actual facts. Though this threat can be avoided, at least for simple mechanical systems, it repays scrutiny; not least because it leads to some open questions.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeMar 12th 2013
    • (edited Mar 12th 2013)

    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…)

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 13th 2013

    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!

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 13th 2013

    One quick thought. So I could instantiate

    XE X XE XE pb X X, \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

    playersofactualteams possibleplayersofactualteams possibleplayersofpossibleteams pb teams possibleteams, \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)?

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeMar 13th 2013

    That sounds right to me.

    And so in this language my above remark that converse Barcan applies when XX 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.

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 13th 2013

    The remark above was

    (XX)(X XX). \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 XX 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

    X XEXE. \underset{X}{\sum} \diamond_X E \to \diamond \underset{X}{\sum} E.

    But the forward Barcan formula holds only for special XX.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeMar 13th 2013

    Yes.

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

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2013

    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 1W 2W_1\to W_2 in a (pre)sheaf model with a span W 1RW 2W_1 \leftarrow R \to W_2, with RR the witnesses of “counterpartness” between pairs of individuals in W 1W_1 and W 2W_2. By passing to a quasitopos of concrete sheaves, you could moreover probably enforce that RW 1×W 2R \to W_1 \times W_2 is monic, so that RR really is a mere relation (rather than containing multiple witnesses of counterpartness for the same two individuals).

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 13th 2013

    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.

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

    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.

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

    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”).

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2013

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

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeMar 14th 2013

    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.

    • CommentRowNumber28.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 14th 2013

    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 P\Box P entails P\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.”

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeMar 14th 2013
    • (edited Mar 14th 2013)

    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 WW “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 nnLab entry to save other people like me from similarly missing this simple fact for so long.

    • CommentRowNumber30.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 14th 2013

    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]{True,False}[0, 1] \to \{True, False\}, where 00 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!

    • CommentRowNumber31.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 14th 2013

    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?

    • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeMar 14th 2013
    • (edited Mar 14th 2013)

    There are some issues here. First, in modal (homotopy) type theory maps AA\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 AA\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.

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2013

    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.

    • CommentRowNumber34.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 14th 2013

    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.

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeMar 15th 2013

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

    • CommentRowNumber36.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 15th 2013

    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.

    • CommentRowNumber37.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 15th 2013

    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¬¬PP \leftrightarrow \not \not P.

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeMar 15th 2013

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

    • CommentRowNumber39.
    • CommentAuthorMike Shulman
    • CommentTimeMar 15th 2013

    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.