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.
Is there some thought with modal type theory to think about its version of the Barcan formula
For example, we could compare
and
If 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.
I agree with the last sentence. In , the is only possible; while in , the 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.
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.
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 be the round trips I can take from . 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 , with a circle, and all 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.
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.
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.
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?
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 as the shape modality, dually.
So first of all, that map
there, which one is it? For a dependent type and interpreted in the categorical semantics of a cohesive -topos we have the maps in
induced from the naturality of the -unit applied to the bundle .
(Sorry if I am being stupid here, I am kind of absorbed by something else right now.)
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?
Urs, so in #9, are you relying on anything special about as a modality other than that it is monadic?
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 to have the interpretation that one thinks it should have is that preserves pullback diagrams of the form displayed above. If that is the case then it follows that the left vertical map is the correct fiberwise -closure, hence that is a closure operator on the slice over .
If 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 -closure is “Galois-ification”, it sends an arbitrary bundle over to one that is -Galois over it (hence is a locally constant -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 -closed types/objects dependent over can be interpreted as all the -stacks over , with respect to a certain canonical étale-type of Grothendieck topology on . In particular the subcategory of the slice on the -closed bundles/dependent types is itself again an -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 -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 happens to be -closed, then there is a natural equivalence
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!)
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).
What did Butterfield say about physics and modality? I don’t know!
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.
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…)
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:
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!
One quick thought. So I could instantiate
with something like
I wonder if that top right entry can be formulated differently
possible players of possible teams = possible (players of teams)?
That sounds right to me.
And so in this language my above remark that converse Barcan applies when is -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.
The remark above was
Doesn’t this say that when is -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 , since there is a natural map
But the forward Barcan formula holds only for special .
Yes.
Oh, I see, I used the term “converse Barcan formula” the wrong way around. Should have paid better attention.
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 in a (pre)sheaf model with a span , with the witnesses of “counterpartness” between pairs of individuals in and . By passing to a quasitopos of concrete sheaves, you could moreover probably enforce that is monic, so that really is a mere relation (rather than containing multiple witnesses of counterpartness for the same two individuals).
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.
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 that makes people think that it accurately reflects a nontrivial portion of the meaning of “possible”?
When I say that “I take 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 which does satisfy all these extra properties, interpreting it indeed as producing shape/fundamental -groupoids is consistent in that it makes a whole bunch of statements involving have a consistent and nontrivial such interpretation for a whole bunch of aspects of the meaning of shape/fundamental -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.
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”).
Heh, #23 could also apply to mathematicians arguing about whether the axiom of choice or the continuum hypothesis are true.
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.
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 entails 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.”
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 “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 Lab entry to save other people like me from similarly missing this simple fact for so long.
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 , where 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!
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?
There are some issues here. First, in modal (homotopy) type theory maps 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
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 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 to be the shape modality and to be then the flat modality, then one has
(since goes to discrete objects and these are the -closed objects). So on the one hand a natural map 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.
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.
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.
There are philosophers who believe there is an absolute nature of “necessity”, independently of how the word is used in human language?
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.
Is there some connection between linking modalities via
and ’classical’ logic? I mean, say you take as monadic modality . Then
So is also a comonad. So the unit and counit give .
Re 36: bizarre! It never would have occurred to me to suppose that “metaphysical necessity” was a meaningful thing.
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.
1 to 39 of 39