Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have given necessity and possibility (which used to redirect to S4-modal logc) an entry of their own.
The entry presently
first recalls the usual axioms;
then complains that these are arguably necessary but not sufficient to characterize the idea of necessity/possibility;
and then points out that if one passes from propositional logic to first-order logic (hyperdoctrines) and/or to dependent type theory, then there is a way to axiomatize modalities that actually have the correct interpretation, namely by forming the reflection (co)monads of and , respectively.
You may possibly complain, but not necessarily. Give it a thought. I was upset about the state of affairs of the insufficient axiomatics considered in modal logic for a long time, and this is my attempt to make my peace with it.
I suppose all I am saying is that possible worlds semantics is naturally realized by the base change operations in hyperdoctrines/dependent type theory.
This must have been stated before somewhere. Where?
I thought I was saying something along those lines here.
The beginning of the article on necessity and possibility speaks about S4; however, if I understand correctly the section “In first-order logic and dependent type theory”, as currently written, it formalizes S5 (as possible worlds semantics with a trivial “accessibility” relation).
That is, to interpret possibility and necessity as a monad-comonad adjoint pair (regardless of whether this comes from an adjoint triple (or is that automatic?)) is not only to demand the S4 axioms, but also the further S5 axioms as well (e.g., that possibility entails necessary possibility: because ) .
I thought the point of the necessity/possibility modalities was to describe the logical behavior of those words intrinsically without having to introduce the “set of possible worlds” explicitly. Are you just saying that a natural semantics of such a logic is given by going back to a set of possible worlds? Surely modal logicians have known that since ever.
Re #4 again, the model is even stronger than the usual S5 models. These are usually set up in terms of an equivalence relation on worlds, known as an ‘accessibility’ relation. Then we say, e.g., holds at a world iff holds at all worlds accessible to . Your model in effect has all worlds in a single equivalence class.
But that reminds me that we’ve been speaking about homotopifying equivalence relations elsewhere, namely, at ’duality in physics’, where we’ve been hearing about, e.g. here, equivalence relations up to coherence as a 1-epimorphisms or effective epimorphisms. (I’d be very interested in Mike’s opinion on that exchange.)
So if modality isn’t determined just by the type of worlds, but also by the accessibility relation, can we see something modal about situations where one type is sent by an effective epimorphism to another, ? Could one have a for a proposition holding coherently in all worlds -accessible to ?
There might be a flip like here
instead of saying
a) that two Lagrangians are dual if there is an equivalence between the QFTs which they induce under quantization,
we may turn this around and say that therefore
b) quantization is the result of forming the homotopy quotient of the space of Lagrangian data by these duality relations.
so that ‘worlds’ are the result of some homotopy quotient.
Mike, re#6, I am saying that
a) S4 just does not capture “the logical behaviour of those words”, as there are simple counterexamples (this should not be contoversial here, we have been discussing all sorts of (co-)monads and S4 claims that they all should be called “necessity” and “possibility”, that’s weird);
b) the evident (it seems to me) actual axiomatization of “the logical behaviour of those words” is via dependent sum and dependent product. That seems to subsume the set-based traditional “possible world semantics”, but is maybe a bit more general. In any case, I am thinking that this (and only this) actually does accurately axiomatize “the logical behaviour of those words”.
Sridar, re#4:
yes, in the same vein: the beginning of the article describes S4 which is usually advertised as axiomatizing “necessity” and “possibility” but which clearly does not, as simple counterexamples show. Then in the second part I say what I think is clearly the right answer.
But S5 still does not cut it. The example of also satisfies S5, but it clearly does not capture the meaning of necessity and possibility.
David, re various remarks:
generally, please feel invited to add to the entry. I may not be aware of all previous discussion, it just struck me the other day that the adjoint pair induced by the base change adjoint triple is the right axiomatization, and I made a note on this.
Specifically re #7: this is captured simply by having base change not to but to some intermediate stage.
Let be some type (“of possible worlds” if you wish) and a morphism, possibly a 1-epimorphism if desired. Then with we have that is true/inhabited at if it is true/inhabited at all in the same fiber of as .
I’ll add that to the entry.
David,
I have added the relative version now here.
To bring this together with the other discussion: this now gives formalization of statements such as
For pre-quantum data to be in the duality class of QFT it is necessary that…
and so forth.
Re #8a, whenever you abstractly axiomatize something, you necessarily expand the class of models from the one or few you were looking at for motivation. That’s one of the points of abstraction. I don’t see why “S4” can be said to “claim” that all these models should be called necessity and possibility; S4 is just a set of axioms about two operations and , which we are free to sometimes interpret as necessity and possibility.
And re #8b, there’s no reason to expect there to be only one “right” way to abstractly axiomatize a particular thing.
Is there ever a time when you want to talk about dual pre-quantum data not sharing properties? So a Calabi-Yau manifold marked with A could be said to be possibly B since there’s a mirror manifold whose B-model yields the same QFT. Perhaps that’s an odd way of speaking. “All prequantum data is possibly B.”
I wonder if there are properties of such (co)monads created through base change and extension that might be said to characterise possibility and necessity better than what’s come out of the S5 axioms.
Back to the S4 inclination, there’s that work by Hamkins and Lowe on The modal logic of forcing. So given a model of set theory we can wonder about whether some or all of its extensions has some property, and then think that it possibly holds or necessarily holds at that model. This is S4.2. Also the future modalities, always from now on, and at some point in the future, behave S4-like.
I’d be very interested in Mike’s opinion on that exchange.
Do I have to read the whole thread? (-: Sorry, I have a tendency to tune out certain threads, and I don’t always notice when they meander in directions that I might be interested in.
Not the whole thread :-).
It’s about the difference between homotopifying equivalence relations as a kind of Cech cover tower and doing it as an effective epimorphism.
23, and then 45-50.
Mike, re #11
if you regard S4 as just some axioms not necessarily related to possibility and necessity, then that’s in accord with what I am thinking but not with that many modal logicians are thinking.
Of course there is flexibility in what to regard as an axiomatization of an informal concept, but S4 alone just won’t axiomatize a sensible concept of necessity (neither do S5 or similar strengthenings):
The (co-)monads constant on False and True, respectively, satisfy S4, but regarding as a sensible formalization of “necessity” means to regard as sensible the sentence “Every proposition is necessarily true.” and in particular the sentence “False is necessarily true.” I don’t believe that any modal logician confronted with this will insist that this is a sensible formalization.
The problem seems to be that many modal logicians haven’t thought about all the things that could be axiomatized by (co-)monads.
David writes:
Also the future modalities, always from now on, and at some point in the future, behave S4-like.
The problem that I am talking about is that every modality behaves S4-like.
We have dozens of entries of examples for this. The problem is hence that S4 is not an axiomatization of the “necessity” modality, but just of any old modality.
In discussion elsewhere Valeria de Paiva informs me that most classical modal logicians actually consider just K modal logic as axiomatizing necessity. That amounts to thinking that every functor axiomatizes necessity.
I think all this is clearly weird and wrong. I am not surprised to hear that some people think differently, but I am surprised that here on the nForum, between the participants of this thread here, we need to spend much time on this. Elsewhere we are discussing plenty of examples of (co-)monads with all kinds of interpretations, but here we need discussion that not all of them axiomatize “necessity”? What’s going on?
I think they’re getting at necessary conditions rather than sufficient ones. But yes you might expect that they’d want to add more features than bare K.
My thought was that the worlds as type solution won’t work if you want to reach those modalities normally modelled on variation over directed sets, such as temporal logic, at least so long as we stick with ordinary (undirected) homotopy types.
I think they’re getting at necessary conditions rather than sufficient ones.
Yes, this is exactly what I wrote into the entry necessity: that the traditional axioms are not sufficient, but that improving the axioms to saying “possibility and necessity is the adjoint pair induced from a base change adjoint triple” does do the job.
Is there any disagreement on that? Before we talk about various other things, I’d rather like to have this sorted out.
[ wrote a message to the wrong thread here. Evidently time to call it quits.]
My impression has been that the intent of modal logic is to capture some aspects of the intuitive meaning of “necessarily” and “possibly”, not to model a particular situation involving possible worlds. Possible worlds are one way to describe a semantics that gives a precise meaning to “necessarily” and “possibly”, but I thought there were (at least arguably) aspects of the intuitive meaning of the latter that they don’t exactly reflect. If that’s right, then I don’t think we should claim that necessity and possibility are axiomatized by a base change adjoint triple.
I’m sure many metaphysicians would reply just like that #22, which may lead people to wonder what it is they have access to that allows them to tell us what “necessarily” and “possibly” really mean. It is also important to remember that there are different communities studying modal logic. In computer science they study all kinds of weak modal logic. From what I saw of it, it seemed a little centipede mathematics-like, but there are various uses of the related formalisms of temporal and dynamic logic in model-checking, and then coalgebraic logic. Finding a computer science application of base change triples is the key there.
But I think it’s what the metaphysicians are doing that’s most mystifying to outsiders. If you’re serious in wanting to understand what’s at stake here, read some analytic metaphysics, for example the SEP entry for possible objects. The appropriateness of those Barcan formulas I once told you about are the kinds of things we may debate, as we see in that quotation I put up yesterday.
Many of these people take metaphysically possible worlds seriously. This is not about physics. Disputes are to be had about modal counterparts and modal dimensionalism (addressed in the SEP article). The discussion revolves around various intuitions, formalisms and semantics.
For the metaphysician we can’t just throw out a new formalism – base change adjoint triples – and hope they’ll bite. You would have to make it speak to their concerns. Actually, I think this quite possible, especially if we get modal types, rather than just propositions, up and running. It seems to me that modal counterparts and dimensionalism are all about fibrations.
re #22:
The axiomatization via base change is not semantics but is syntax, as you know. For base change along an effective epi its natural semantics includes the one known as possible worlds semantics, but it is much more general.
Whether or not the axiomatization via base change is what everyone will agree on, at least it arguably captures the actual meaning of “necessity” while K, T, S4 and S5 demonstrably do not. Hence whoever finds the axiomatization via base change unsatisfactory has to produce something else. Falling back to S4 just begs the question. S4 axiomatizes modality, not necessity.
re #23:
Finding a computer science application of base change triples is the key there.
It’s used all over the place. In Coq this are the basic operations.
But I think it’s what the metaphysicians are doing that’s most mystifying to outsiders. If you’re serious in wanting to understand what’s at stake here, read some analytic metaphysics, for example the SEP entry for possible objects.
I did read that. But I would rather we adopt for the time being an argument more in the style of mathematics, where we trust that we may understand a concept – and a rather simple one as it were – by way of reasoning, and not by falling back to proof by authority.
I’m a little lost as to who you think will be interested in this base change account if not metaphysicians. I am for a strange combination of reasons, some of which include luring philosophers to realise that their formal tools are inadequate for their own (not my) purposes.
Computer scientist modal logicians will carry on doing their work generally with weaker modal systems, some as an abstract game, some with a view to computer science applications. But perhaps they might like to see if modal type theory has something to offer.
The only people that write seriously on the topic of necessity and possibility as such are metaphysicians. Some philosophers think the whole subject rather silly, but others think there’s a fact of the matter in getting our ideas of possibility and necessity sorted out. These kinds of people wrestle with issues such as the logical relation between it possibly being the case that there is something which is P and it being the case that there is something which is possibly P. Some use possible worlds talk as a means to help intuitions, others seem to believe in their existence. For example, one big name, David Lewis, thought that the best sense we could make of the truth of ’X could have had eggs for breakfast’ is that in some close world a modal counterpart of X had eggs for breakfast.
As for my weird position, beside wishing to show philosophers a shiny new tool (thus making them realise what they’ve missed out on by not following maths through the 20th century), there is the odd phenomenon that some of the issues philosophers have encountered make contact with some of those we have encountered, such as the famous meets dependent types problem. I wouldn’t mind betting that as we thought through modal types (not just propositions) dependent on Worlds, then we’d meet some of the issues metaphysicians have stumbled upon concerning modal counterparts.
But who else? Does your everyday use of ’necessary’ and ’possibly’ now look different to you? Do you now understand more fully what it means to say ’Emeralds are necessarily green’? Or, ’I can’t be in two places at once’?
S4 axiomatizes modality, not necessity.
This is a good observation.
Intuitive meaning of necessity is about necessary statement, necessary truth. When one intuitively thinks that something must hold, one does not think that it holds for all something as his intuition does not capture the wholeness, or even the collection-like notion of a pre-existing pool where the truth evaluable statements surface from. One rather thinks of evaluation or test of statement given, once it is at evaluable stage. Achieveing the stage is not necessarily choosing from a pool of class of possibilities, nor it presuposes the class. So, is it true that the intuitive concept of evaluation must satisfy the base change axiomatization ?
I do not fully understand a situation where forall is in the sense of probability one. Is there a difference between probability zero occurence and nonexistent occurence ? In standard forcing, truly nonexistent occurence is not a notion, it is stretching beyond the internally expressible notion. But I can imagine, that it is possible to axiomatize the logic which distinguishes nonexistent from probability zero. But the richer axiomatics as Urs suggests seems to prohibit such a situation. In my language the evaluative test can do what internal logic of probabilistic necessity can not express. I still believe that some other extension can have this allowed and even the whole hierarchy of internalization constraints on necessity. The probability encompasses more wholesome evaluation than the single occurence. The difference between internal and external for forcing makes a difference, it seems to me.
I’m a little lost as to who you think will be interested in this base change account if not metaphysicians.
Me. :-)
I see people talk about axiomatizing necessity and possibility, and it bugs me because they seem to do it wrong in that they say “necessity” for things that I spent much energy on demonstrating that they have meaning, but a very different one.
So I want to understand – for myself, for the pursuit of truth – what a decent axiomatization of necessity would be. I think I found it, and I think it’s rather clear.
With that in hand, I now feel I may go and sort out all these issues that people discuss.
These kinds of people wrestle with issues such as the logical relation between it possibly being the case that there is something which is P and it being the case that there is something which is possibly P.
The first thing that a decent axiomatization of possibility and necessity gives is a check if the question parses. For the above, direct translation to symbols yields
and
We see however that this does not type-check, as operates in context while is in context (notation as in the entry). One way to fix this is to extend the context back from to , this gives
and
.
Now these expressions parse and may be compared. It turns out that they are judgementally equal.
Is that the right translation? It’s
is a predicate associated to some category of things. One might proceed:
Then there’s the problem whether to take as dependent. Maybe
and so
Then we compare and the other seems problematic unless there’s an idea of counterparts, where we transport an in one world to another.
Sorry, no time. Have to dash, shouldn’t have started this.
Is that the right translation?
The good thing is that whatever translation is preferred, we may now analyze it.
So you suggest to consider instead the relation between
and
(which is just shorthand for and , respectively).
Expanding out, this is
and
Again, both terms are judgementally equal.
shouldn’t have started this.
I think this is very good, to get a feeling for what’s going on.
Another snatched moment. You can do that if Things is dependent on Worlds? There’s no need to worry about how a thing of one world would be transported along the accessibility relation of worlds?
Trying things out:
and
I have no more time for this discussion, but I will just say that the only thing I have to quibble with at necessity is the end conclusion “This accurately reflects the intended informal concepts.” I don’t think we should assert that it accurately reflects — or, at least, completely reflects — the intended informal concepts of “necessity” and “possibility”; it accurately reflects the intended concepts of “in all possible worlds” and “in some possible world” based on an equivalence relation of accessibility between worlds, but I don’t think it’s necessary (heh) that the informal words “necessary” and “possible” have to be interpreted as referring to “possible worlds” at all. That’s what I was trying to say in 22.
To point to one of those who, like I said in #26, think the whole subject rather silly, Peter Hacker in Why Study Philosophy? writes:
Physicists study matter, motion, and energy. Chemists study substances and their forms of combination, interaction and decomposition. Biologists study living things. And so forth. But what is it that philosophers study? One answer common throughout the ages is that as physicists study physics, philosophers study meta-physics. Philosophers, or at any rate the deepest of philosophers, we are told, are meta-physicists. Physicists study the contingencies of the world – things that happen to be so. Meta-physicists study the essential, necessary features of all possible worlds.
This reply is unconvincing for a number of reasons. For one thing, if it were the case, it would need a great deal of explaining to vindicate philosophy. For while physics has produced libraries of well established results (and chemistry and biology yet more libraries), we can look in vain for trustworthy books entitled Established Truths of Metaphysics or A Handbook of Philosophical Facts.
Moreover, there is more than an air of absurdity to the thought that chemists discover that water consists of H2O, and that philosophers then discover that this is not a contingent truth, but a necessary one; or that physicists discover that E=mc2, and meta-physicists then discover that this is true in all possible worlds.
Finally, if we look at the kinds of results that meta-physicists do produce, it is evident that they are little more than paradox (time is unreal; solid objects are not really solid; coloured objects are not really coloured), absurdity (we cannot know the thoughts or intentions of another; we are nothing more than a bundle of perceptions) and systematically contested to boot (there are or are not universals; moral truths are all absolute or all relative). So let us discard this foolishness.
Metaphysics is an illusion that besets philosophers (and philosophically-minded scientists) from generation to generation, which it is the task of good philosophy to dispel.
And elsewhere on how to think about necessity properly:
Do you think that Wittgenstein’s philosophical method is a kind of Copernican revolution in philosophy?
I think one might say something like that. Kant characterized his critical philosophy as effecting a Copernican revolution. All previous philosophy had insisted that the mind must conform to the nature of things; but Kant suggested that phenomenal things [things as experienced] must conform to the nature of the human mind. In particular, phenomenal objects must conform to the ‘synthetic a priori principles’ which are conditions of the possibility of experience. Synthetic a priori principles are conceived to be propositions that are both necessary, and true of physical reality. Wittgenstein’s account of the nature of necessary propositions effects a second Copernican revolution. He argued that a priori propositions appear to describe how things necessarily are, but in fact they do no such thing. The necessary truths of logic are vacuous tautologies that one and all say nothing at all. But each such tautology is internally related to an inference rule. Other necessary truths, that appear to fit the category of the synthetic a priori in that they are necessary but not analytic – such as ‘nothing can be red and green all over simultaneously’ or ‘red is more like orange than it is like yellow’ are what he called ‘grammatical propositions’. They are, in effect, norms of representation – rules for the use of the constituent terms in the guise of descriptions. That red is more like orange than it is like yellow is actually no more than an inference rule: it entitles one to infer that if A is red, B orange and C yellow, then A is more like B in colour than it is like C. And these internal relations are partly constitutive of what it is to be red, or orange, or yellow. Similarly, the principle that every event has a cause is part of the grammar of ‘event’ in certain physical systems, eg Newtonian mechanics – it is a ‘norm of representation’. That every event is spatio-temporally related to every other event is not a description of a physical fact, nor yet of a metaphysical fact, but a ‘grammatical’ truth partly definitive of the term ‘event’: we would not count something as a genuine event if it were not simultaneous with, antecedent to, or subsequent to any other events you care to mention. We are prone to take such grammatical propositions to be descriptions of objective necessities in the world. That is indeed what they seem to be. But they seem so only because these grammatical propositions that are expressions of rules or conventions of representation, cast a shadow upon the world, and we confuse the shadow for a reality. I think Wittgenstein did more to demystify the nature of necessity than any other thinker.
Mike, re #33,
okay, thanks. I have changed that line to now read as follows:
This accurately reflects the informal concept of “possibly true in some cases” and “necessarily true in all cases” (or “in some worlds”/”in all worlds”, if one wishes).
David, re #31,
if Things depend on Worlds, then
parses and yields the total space of context extended back to Worlds.
But now
does not type-check anymore, as it is not clear what is to mean. Because is in the context of Things (which in turn are in the context of Worlds) but the operator expects something in just the context of Worlds.
So one would have to base change to the context of just Worlds first. There are two options for this, either via dependent sum/exists, or via dependent product/forall. One would have to decide which one of these reflects the informal statement that one wishes to formalize.
David, re #34,
it seems to me that modal logic (to concentrate on this aspect of philosophy, if it is one) could potentially be a sophisticated subject, but that what has been done here (as far as I see) falls short of what one could potentially do.
Much like natural philosophy was mostly silly before some researcher from the UK finally figured out what the darn rules of the subject actually are. In retrospect it was not natural philosophy as a subject that was silly, but the naivety with which it was persued. Similar comments might apply to alchemy etc.
This is partly what made me start this thread here. We have been discussing here, over the years, nontrivial business with almost a dozen different modalities, but when one carries this discussion to people who say they study modal logic, one finds that beyond very vague speaking about “necessity” there is little to connect to. Therefore I wanted to sort out this business with possibility and necessity once and for all, from the perspective at least that we have been studying here.
One thing I like about the formalization of possibility and necessity via base change is that, conversely, it may be thought of as a description of base change via modality. So this gives a neat unifying modal picture that complements that of cohesion.
Namely before we start adding cohesion, we are already on a backdrop of dependent type theory. Speaking modally this means that even “before” there is a “category of being”, there is already a “category of possibility”. Which is kind of enjoyable, in a way.
So sorry to interrupt this interesting conversation. I was just amused by “some researcher from the UK” as I guess Urs means Newton, but he wasn’t really from the UK, was he? I think they just called it England. I had to look some of this up, stuff that surely any UK child today knows, that the first Acts of Union were passed in 1707 while Newton was still alive, but even so the term ’UK’ then was rarely if ever used during the 18th century – Great Britain was used, apparently. The term UK became prominent in the 19th century after the union of Great Britain and Ireland in 1801.
Urs, 27 was question to you. It is a bit dense, I know, but I hope I wrote it fairly clearly, after a long effort.
Todd, yes, that’s right, I meant Newton. Currently I am writing an application for a UK research grant and the instructions for that keep asking me to highlight related researchers in the UK. I am getting to the point that I end all of my sentences with a reference to some researcher in the UK ;-)
Zoran, sorry for not replying to #27 earlier.
I see two aspects there:
First, if you come up with a proposal for an axiomatization of “possibility”/”necessity” that is sensible and different from the proposal via base change, then I won’t complain. It would be good to see it. All I am complaining about is calling K, T, S4, S5, … an axiomatization of possibility/necessity, because these axioms are verified by modalities that very clearly do not sensibly have the interpretation of possibility/necessity, not by any stretch. So something must be added to these axioms.
Second, you seem to suggest that given a probability space, then we might want to speak of “necessarily” in the technical sence of “almost surely”. That’s an interesting thought. Let me think about how one might try to formalize this…
Ok, after small detour #34-35, back to work on #37.
So one would have to base change to the context of just Worlds first. There are two options for this, either via dependent sum/exists, or via dependent product/forall.
The natural choice would be dependent sum, I’d think. So we take first to ’Worlds with a ’, and then apply to give worlds for which some related world possesses a .
But that’s odd, since we have
and have now modified
to
which (a) now doesn’t parse at the beginning, and (b) the end of the term is now the same as the one we’re comparing it to, (1).
So (A) we go back to Williamson and realise we should be quantifying over possible things, , and then saying something like ’There’s a possible thing which is ’.
But why do we not see alternative (B) use sheaf semantics, like Awodey and Kishida, which allows counterparts for individuals in neighbouring worlds?
(A) seems like, given , one has an equivalence
re Zoran’s remark in #27 and re #42:
I see that people of course considered “modal probabibilistic logic”. But I’d much rather see that it comes out as a special case of the base change axiomatics after all.
The usual way to incorporate measure theory and the neglect of stuff supported on measure 0 is to pass to toposes of “almost everywhere covers”, as in section 3.2 of Jackson 06. That would seem to be the right context to speak of probabiliy theory in the present situation. And I’d think that here base change shows precisely the behaviour that you suggested one could consider in the context of probability theory, in that statements will be true in the inernal logic if they hold away froma set of measure zero on the given site of definition.
David, re #35:
I’d be surprised if we couldn’t reduce all concepts of necessity to the “possible worlds”-way of speaking. Indeed it seems to me that only after stating what the possibilities are meant to be does it make sense to speak about necessity etc. For instance the example in #35 which is alluded to by
Other necessary truths, that appear to fit the category of the synthetic a priori in that they are necessary but not analytic – such as ‘nothing can be red and green all over simultaneously’
seem to easily reduce in any given formalization of “things with color” to the evident statement that .
Funny you mention that example since part of the revival of Hegel thinks he was onto something with his idea of ’determinate negation’. I’m still trying to get a sense of this, but there’s an idea that with Frege’s reduction of negation to an operation acting only on propositions, something was lost, and that negation of predicates should be possible.
To the extent that I was successful understanding the idea, it seemed to be useful to think of
and so on.
David, re #43:
if we find a term in a smaller context hit with an operator assuming a larger context then it makes sense to assume that a context extension is silently implied. If we apply this rule to then it parses, but now comes out being different from .
re #44:
Yes, so is in context . The first expression translates to the pullback
computing this as two consecutive pullbacks by the pasting law produces the second expression
David, re #47:
could you give me a text passage in Hegel that this here would refer to:
part of the revival of Hegel thinks he was onto something with his idea of ’determinate negation’
Because under our running -dictionary Hegel’s “determinate” (“bestimmt”) translates to “at a higher level” in the essential subtopos lattice.
For instance Hegel’s “pure being” is the right adjoint in and the determination of that to “determinate being” is the right adjoint of the higher in the sense defined at Aufhebung.
That’s anyway how “we” currently read it, following that page 21 or the like of “Some thoughts on the future of category theory”.
Re #48, so perhaps one solution to Barcan issues is that a reasonable way to parse the two sides is to turn them into something clearly equivalent.
’There is a possible thing which is P’ and ’Possibly there is a P’.
I’d still like to see where Awodey-Kishida semantics feature. They seem to rely on for the Worlds and transport between them. I wonder if in a sense they’re using your cohesive modalities.
Re #49, let’s start a new thread on determinate negation.
So what are Awodey and Kishida doing? They’re forming models of (untyped) first-order modal logic as sheaves (of individuals) over a space of worlds. Necessity applied to a proposition is the interior of the subspace of worlds where that proposition holds, while applied to a predicate, it’s the interior of the subspace of the total space determined by the predicate, etc.
Can we understand this in a cohesive setting? Is there a formal construction of the interior of a subtype of a type?
So what are Awodey and Kishida doing?
They give a model of S4 in sheaf toposes over a topological space. My running complaint is that S4 does not necessarily axiomatize possibility/necessity but (just) modality as such. Indeed, as you say, their model is more related to , I think.
Perhaps they care less for the metaphysical interpretation and more for finding some kind of semantics which is complete for the logic, first order S4. There’s still the question of why that particular choice of semantics worked.
On the other hand, there is a rich tradition in philosophy of considering extra structure on the collection of possible worlds. Some even invoke a metric structure, such as when considering counterfactuals.
One may say “Had Peter taken an aspirin, he would no longer have a headache”. You might think of using your possible worlds to think whether in all worlds where Peter took an aspirin, he doesn’t have a headache. This raises the issue of what ’Peter’ would refer to in other worlds. But imagine we’ve sorted that out, even then we wouldn’t want to look at all possible worlds in which he takes an aspirin. There might be one rather distinct from ours, where everyone has a headache induced in them permanently by some evil beings which can’t be touched by an aspirin. The intuition is then that we should consider the ’closest’ possible world in which he took the aspirin, a world as similar to ours as possible except for the detail of the taken aspirin.
How one is supposed to think of these things is not clear. Surely we can imagine a minimally modified world which ends up very different from ours. Anyway, that general sense that we can think of degrees of variation between worlds is a common one, and it did play a role in Judea Pearl’s work on counterfactuals, see sec 7.4 of his book Causality.
So maybe the idea of using cohesive modalities, and even differential cohesive ones (doesn’t Awodey and Kishida’s etale spaces suggest that?), isn’t so surprising.
Second, you seem to suggest that given a probability space, then we might want to speak of “necessarily” in the technical sence of “almost surely”. That’s an interesting thought.
This is the standard idea from Cohen and later in the forcing method in model theory. What I say is that internally there is no difference, but externally there is a difference. So I imagine a situation where external and internal differ so we have two levels of necessity.
There’s still the question of why that particular choice of semantics worked.
I am not sure what you mean by this. Do you mean why some nilpotent monad happens to exist? It seems to me that there are plenty, and if one considers any particular one it would be nice to say what makes one consider this one instead of another one.
On the other hand, there is a rich tradition in philosophy of considering extra structure on the collection of possible worlds. Some even invoke a metric structure, such as when considering counterfactuals.
With the axiomatization via base change, the collection of possible worlds may be any object in any locally Cartesian closed infinity-category, in particular in any infinity-topos. It could be a space with any kind of geometry that one likes. Via the axiomatization via base change, we will know in each case precisely what it means for something to be possible that is parameterized over, say, a derived Deligne-Mumford stack of possible worlds.
Or since you mention cohesion: generically a proposition dependent on a cohesive space of possibilities is unlikely to be necessary, because that means regarded as a cohesive bundle over it has a global section, and that is generically not the case. However the image of that proposition under the or the modality, dependent now on the discretely cohesive space , has much greater chances to be necessary.
What you mention as the kind of example one might like to formalize is reminiscent of Zoran’s comment in #27, which I replied to in #45. There the idea is to call something necessary if it is true “almost always”. I think this is neatly handled by passing to the respective topos which embodies the relevant concept of locality, namely the sheaf topos over the “almost everywhere covers” of the underlying probability space.
In the example that you consider similar constructions might do what one wants. It seems to me that where you say
How one is supposed to think of these things is not clear.
this characterizes quite generally the extra effort that it takes to go from vague informal speaking to precise formalization: in this process one often notices that the vague informal speaking was ambiguous and that one needs to sort out what one really wants to mean. The formalization helps sharpen the intellectual analysis of the problem. If one finds that this requires work then this is a good sign, I would say, because it signals progress. Because when speaking about possibilies of headaches, one is talking about immensely complex systems. For such talk to be more than the usual everyday chat, one will need to decide beforehand which aspects of the observable universe one does want to mean to consider. A full description will have to take into account quantum effects in Peter’s synapses and fully formalizing that seems more ambitious than what physicists mean when they are being ridiculed for speaking of “theories of everything”. The implication is, it seems to me, that if somebody really wants to seriously formalize the possibility of headaches in reaction to medicamentation, then it is first of all that somebody’s task to characterize the model of reality that is supposed to be used.
Zoran, did you see my reply to you in #45?
Take the topos over the site of “almost everywhere covers” of the given probability space. Necessity/possibility in there expressed via base change will express the “almost surely”-version. Now consider the image of the situation under the global section geometric morphism in . Then necessity/possibility in there expressed via base change is the “external” version.
I would say that captures what you are after. If not, you may need to give me more data.
Sorry, I have not seen 45. Are you saying that for both notions you can use the same notion of pullbacks in the same universe, just you take different covers in the same universe ? That would imply that both modalities can be considered in the same model with the same pullbacks (just with multiple modality symbols and different covers). Or you are just saying the weaker statement that in the same universe you can make internal topoi for which this is true separately (that is trivial, and implied by model theory).
All I mean ist to speak of sheaves (“of possibilities”) in a sheaf topos over almost everywhere covers, and of their underlying sets . Or something like this, dependig on what you want. I am not making a deep statement here, just pointing out that “almost everywhere truth” is the internal truth in such sheaf toposes.
I am not sure what you mean by this.
I meant, if S4 is a theory of modality as such, why did their choice of models with a specific interpretation of the modality turn out to be complete for it? Other choices wouldn’t have been complete.
That sounds interesting looking for different settings to see what base change looks like there.
I am not making a deep statement here, just pointing out that “almost everywhere truth” is the internal truth in such sheaf toposes.
Yes, this is the rephrasing of forcing done in topos language (as most people nowdays do). But this model does not have the usual necessity expressed in the same topos. One can imagine that most modalities of necessity and necessity in probabilistic sense exist in the same universe. What was my original idea is that I suspect that one can not use the pullbacks for both necessity notions in the same topos. On the other hand, it seems to me that both still stay modalities and both have intuitive meaning of necessity.
If in a model both will exist simultaneously, one of them will not have your intended extension of the modality. But never mind, once I have time I will try to make simultaneous model and then we can discuss. Now it is getting to vague, let’s postpone this side issue…
why did their choice of models with a specific interpretation of the modality turn out to be complete for it? Other choices wouldn’t have been complete.
I suppose I missed that point. Could you elaborate? (Am a bit time pressured here…)
Re #63, not a big deal, but they show the kind of completeness result where with respect to a specific variety of models, if the interpretation of a sentence is contained in the interpretation of another sentence for every model, then in FOS4.
Thanks, I’ should look into this. This might be related to the discussion in the other thread on “Aufhebung” regarding maximal modalities. I still wouldn’t see though that this has any implication on the interpretation of a given modality as “necessity”.
Urs, Sorry, if this is not the way of conducting conversations here. I am a newbie. But I disagree with #1, item 2 “not sufficient to characterize the idea of necessity/possibility”; There isn’t a single notion of necessity/possibility, there is a plurality of them. Talking about it as a single entity (“the idea of necessity/possibility”) doesn’t help. I added a thought about it the entry. Then about item 3 “there is a way to axiomatize modalities that actually have the correct interpretation, namely by forming the reflection (co)monads of ∃\exists and ∀\forall, respectively.” Well, there is a modality there, which might be “the correct interpretation” for you. It is far from being “the correct” for most people I know, it is only “a” correct/reasonable/sensible interpretation. But granted, it is an interesting modality and you want to talk about it. Anyway then there is a mistake where you say that “For every modality one typically demands that it preserves implication in that” the first line is correct, preservation of implication does correspond to distribution of box over arrow. but this is not equivalent to functoriality of diamond. It might be equivalent in classical modal logic, but not in constructive modal logic. it’s the usual phenomenon of many ways of “constructivizing” something that classically is a single thing.
Welcome Valeria! FYI, you can make math code here with pseudo-latex syntax; click “Source” on someone else’s comment to see their input.
I think your first point is exactly what I and others have been saying here in comment #22 and others.
I don’t quite understand your second point; I thought that and were both forms of “preserving implication” — the first says that preserves implication, and the second says that preserves implication.
If you allow me to repeat yet once more, the issue I am bringing up is not that there is no freedom in formalizing necessity, but that clearly not any old comonad expresses necessity. The exponential modality in linear logic, the flat modality in cohesion for instance are not sensibly thought of as expressing necessity.
the issue I am bringing up is not that there is no freedom in formalizing necessity, but that clearly not any old comonad expresses necessity.
I think we all agree on this; the problem is that the page as written did seem to be claiming that there is no freedom in formalizing necessity, i.e. that the “correct” way to do it is using base change. I’ve edited the page some to try to make its claims more justifiable.
I also fixed what seemed to me to be an error: in the trivial adjoint pair of modalities , it’s that’s the comonad and that’s the monad. Hence if we were to use those to interpret necessity and possibility, we would conclude that nothing is necessarily true and everything is possibly true: not very interesting perhaps, but not, I think, an inconsistent interpretation of the intuitive meanings of the words – someone with a highly active imagination might very well believe those statements. (-:
I think if using to model S5, it must be that is the monad and is the comonad, since the monad is meant to be the left adjoint and the comonad the right adjoint. Which is fine; there is indeed one situation in which arises as the monad and as the comonad: for example, following the article’s approach, we could take this as the monad comonad adjunction arising as from an adjoint triple where for any category with initial and terminal objects. In this case, and are both endofunctors of the trivial one-object category. Which would indeed be the space of propositions indexed by possible worlds, if there were no possible worlds (the powerset of the emptyset being the one-object set). This would not mean nothing is necessarily true and everything is possibly true; rather, the opposite: everything is necessarily true and nothing is possibly true. ( itself could remain nontrivial, amounting to the propositions which are not indexed by possible worlds). And I would not take this model to mean there was something wrong with the axioms, any more than I would take the existence of the one-object Boolean algebra to mean there was something wrong with any standard axiomatization of classical propositional logic.
Monad and comonad don’t necessarily align with left and right adjoints, as explained at adjoint modality. What must happen though is that the counit of the comonad is followed by the unit of the monad. In this case, these are
Monad and comonad can do whatever they like in general, but in the context of S5, is a monad, is a comonad, and we have the adjunction (at least, all up to preorder reflection, the S5 axioms not typically being stated in categorified fashion…).
I’ll note again that, though Urs used the unacceptability of (as a model of possibility necessity) to illustrate his base change account as remedying the deficiencies of mere S4 or S5, it is actually the case that still has a base change model (context extension where the new context is empty)…
hi Mike, thanks for the welcoming.
I totally agree with what you’re saying in #22. Thanks for the rewriting on that.
But the point about preservation of implication is exactly that is not a sufficient form of “preserving implication”. Because is not exactly dual to in intuitionsitic logic, is more fundamental, as you only need it to be a monoidal comonad, ie . But the needs to be strong with respect to the , as we show (Gavin Bierman and myself) in pages 26-27 of our paper on S4, which you can find in the blog post http://logic-forall.blogspot.com/2014/12/k-for-kripke.html. It is true that diamond will satisfy the implication you want in the case of S4, but it’s not enough to say that, without saying the preservation of implication by . Intuitionsitic logic is much less symmetric than classical logic and this fact (that simply saying is not enough to get preservation of implication) was known to traditional logicians too. We just re-discovered it in the case of categorical models.
And I will confess that by now I am by now totally confused with the empty monad and comonad. I thought that the function sending everything to True was the comonad and everything to False was the monad, but I get very easyly confused on those issues of left and right.
Now there is another issue with the talking about possible worlds in that, if you do want to do intuitionistic or constructive modal logics, then the Kripke semantics has to be more complicated than you guys are describing it.
This is because you need one accessibility relation for the the intuitionistic basis and one for the modality itself. this http://homepages.inf.ed.ac.uk/gdp/publications/Framework_Int_Modal_Logics.pdf very old paper of Plotkin and Stirling described some of the choices possible.
Finally to use Circle for another right adjoint to Box seems to me a poor choice, as Circle is usually used already for a modality between possibility and necessity that corresponds to the T-monad of the computational lambda calculus (Computational Types from a LogicalPerspective, JFP in the same blog post above).
The point is that boxes usually distribute over conjunctions, diamonds distribute over disjunctions, but T is a ’confused’ modality that behaves a bit like diamond , but it also distributes over conjunctions…
is not only “not enough”; we surely don’t even want it axiomatized in the first place (even classical S5 wouldn’t demand it, for example; in that context, it would have the consequence of making possibility entail necessity (consider what happens when is falsehood), thus collapsing both modalities into identity). What we want is (or, just as well, ).
Axiomatizing is (within the rest of the usual background framework) a roundabout way of axiomatizing that preserves products. But we wouldn’t want the same replacing with throughout; typically preserves coproducts, not products.
It is just a fact that the functor sending everything to is a comonad and not a monad, and the functor sending everything to is a monad and not a comonad. A comonad comes with a counit map , while a monad comes with a unit map , and we have maps and but not (in general) the othe way around. Since S4 and S5 include the axioms and , it must be that is a comonad and a monad. Moreover, the presence of “” also implies that “everything is necessarily true” is impossible unless everything is also true, which would be a very degenerate logic.
I also thought at first that this adjunction ought to arise from a base change where there are no possible worlds, but I’m pretty sure this is not the case. It is true that for the adjunction where , with the comonad and monad are constant at and respectively, so this does give rise to that adjoint pair of modalities on . However, the adjoint pair that Urs is talking about is not that one, but rather the comonad and monad on . Indeed, it must be the case that a general proposition depends on , because in order to form meaning “ holds in all possible worlds” we must have the information about which worlds holds in. Thus, the logic on which the modal operators act must be the slice category over , not over . And so if , the entire logic becomes trivial.
On reading again, I see that you (Sridhar) were perhaps talking only about the trivial logic. Okay, but Urs’ point was that the adjunction satisfies S4 even if the logic is not trivial.
Re: 72, I didn’t think anyone had claimed that alone was a sufficient axiom. What I was trying to say in #66, and what I thought Urs was saying on the page, is precisely that we need them both: the first says that preserves implication and the second says that does.
Re: #75: Sure, but the only way to use either of or as either of or in S4 is in a trivial logic:
If you take to be necessity (“everything is necessary”), then you have that even falsehood is necessary, which entails falsehood simpliciter (by , a property present already in modal logic T), which means the logic is trivial.
If you take to be possibility (“everything is possible”), then you have that even falsehood is possible, which entails falsehood simpliciter (by preserving (finitary) coproducts, a property present already in modal logic K), which means the logic is trivial.
If you take to be necessity (“nothing is necessary”), then you have that even truthhood is not necessary, which contradicts the fact that truthhood is necessary (by preserving (finitary) products, a property present already in modal logic K), which means the logic is trivial.
If you take to be possibility (“nothing is possible”), then you have that even truthhood is not possible, which contradicts the fact that truthhood is possible (by , a property present already in modal logic T), which means the logic is trivial.
And as for the adjunction , the adjointness is only relevant when we move beyond S4 to S5, where we have that is the left adjoint and a monad, while is the right adjoint and a comonad. That is part of what I was trying to clarify.
Re: #76: is not merely insufficient, but in fact erroneous (as noted in #74). We do not want this to be provable in general (for example, in terms of possible world semantics: just because there’s some possible world where p implies q, and another possible world where p holds, doesn’t mean there’s some possible world where both hold simultaneously and thus so does q). What we want instead (in any system extending K) are and that preserves (finitary) coproducts.
Why does preserve finite coproducts (and finite products)?
Re 76, Ah, interesting. Sorry, I hadn’t gotten to 74 yet in reading the discussion. That’s weird, though, because I would have thought that if then , and if that’s true then follows (unless I’m still confused). If the truth of entails that is possible, then oughtn’t the possibility of also to entail the possibility of ?
Re: 79, one answer is by consideration of “possible worlds” semantics. Take to be a locally cartesian closed category, and take and to be parallel maps to within it, thought of as an internal binary relation on (thus, usually jointly monic, but it doesn’t matter). Define as the endofunctor of given by pulling back along followed by the right adjoint to ; similarly, define as the endofunctor of given by pulling back along followed by the left adjoint to . This is a general “possible worlds” model of modal logic ; note that is a right adjoint and thus preserves (all) products, while is a left adjoint and thus preserves (all) coproducts. (The left adjoint to is , where is the “converse” relation to ; i.e., the result of swapping the roles of and . Similarly, the right adjoint to is )
Further imposing axiom corresponds to making internal relation reflexive (so that we get and dually ); imposing axiom corresponds to making internal relation transitive (so that we get and dually ). Imposing both (e.g., taking and to be the domain and codomain maps of an internal category) yields . Imposing symmetry makes equivalent to , and dually equivalent to , so that we have the adjunction . Axiom as modal logicians usually state it has an isolated significance too silly to bother with, but is also equivalent to adding the aforementioned symmetry on top of (e.g., taking and to be the domain and codomain maps of an internal groupoid).
But none of that last paragraph matters for the product/coproduct preservation; all of that preservation is already present in possible worlds models of (i.e., no matter what is), by the fact that is a right adjoint and is a left adjoint (though not generally to each other).
That having been said, perhaps you don’t want such a semantic answer. In which case, the only answer is that these exactness properties are part of the rules of (or , or what have you); they’re true by definition. Of course, the ordinary rules only deal with finitary logic, and thus only give finitary exactness properties (opening the door for more general models than those considered above; e.g., can be modeled with as interior and as closure over any topological space, not just Alexandrov spaces).
The exactness properties may not be obvious on the way these logics are normally presented, so I’ll work out the details:
First, let’s show that preserves products; traditional logicians don’t categorify anything, so this amounts to showing entailments in both directions between and . Our basic rules will be “generalization” (by which I mean the rule: from , conclude ) and “modus ponens under ” (by which I mean the axiom: ). [In some sense, my point is that this isn’t the clearest way to axiomatize , but it’s what you’ll find everywhere, including the nLab’s own page on it….]
The left to right directions are easy; they follow from the fact that yields (more explicitly, yields , which yields by “generalization”, which in tandem with “modus ponens under ” yields ); i.e., is functorial.
For the right to left directions, it suffices to handle the nullary and binary cases. Right to left for the nullary case asks us to demonstrate , which is to say, . This follows by applying “generalization” to trivial . Right to left for the binary case asks us to demonstrate . This follows by using the functoriality of to get , and then finishing off with “modus ponens under ”.
Phew. That takes care of preserving finite products. What about preserving finite coproducts? Well, classically, one postulates that is equivalent to , and then the finitary coproduct-preservation of is the same as the finitary product-preservation of . Intuitionistically, we would not want to make this identification, of course, but what we should do instead is… directly postulate the finitary coproduct-preservation of .
Re: 80, it’s not the case that “if then ”, not even if we go all the way to classical . This rule is equivalent to axiom when is empty, but not valid for general . Instead, what we have in is “if , then ”. (In already, we have “if , then ”)
Huh. Your rule “generalization” doesn’t make any sense to me; why would everything that’s true be necessarily true?
Re 82, I’m asking at an intuitive level, why wouldn’t you include that rule?
Re: 83, to assert “” is to assert that entails generically, regardless of world. It is not merely to assert that happens to come out true on some particular possible world we live on right now though it may come out false elsewhere; it is to assert that entails here, there, and everywhere. Thus, to assert is to assert that holds here, there, and everywhere, from which one might as well conclude as well (that no matter where you are, no matter what possible worlds you see, holds on them as well).
Put another way, your question is like asking “Why should we be able to conclude from ? Just because holds for some doesn’t mean it holds universally”. The answer in this case is much like the answer in that case, for is much like .
(Note that I am not saying we should have as a theorem! [Just as we would not have as a theorem])
Re: 84: For example, holds trivially (by explosion), but one doesn’t want to be able to reason from and to (suppose is something contingently false, by which I mean, actually false but possibly true (e.g., that Obama loses the 2012 election), and is something impossible; then both premises hold but the conclusion is false).
For what it’s worth, as noted above, the axiomatization of I was using above (including the “generalization” rule) is the one on nLab’s own page on it: the logic K(m) (although it is written there using instead of )
Huh. So how do I say in modal logic that a closed proposition holds in this world, without asserting anything about other worlds?
For example, holds trivially (by explosion), but one doesn’t want to be able to reason from and to (suppose is something contingently false, by which I mean, actually false but possibly true (e.g., that Obama loses the 2012 election), and is something impossible; then both premises hold but the conclusion is false).
But according to your response to 83, means that is false “generically, i.e. regardless of world”. So in particular, if we have and , then must be false in the world where is true, and therefore holds in that world as well.
Re: 87, The proposition itself represents that claim, internally to the logic. If you want an external judgement, I might write or to mean “ holds at world ”, and then fix some notation to stand for the “actual” world.
Of course, one can use the plain “” symbol however one likes. It’s just notation; bend it to your will. The important point is that it’s easiest to axiomatize the modal logics making use of the notion of generic (world-independent) entailment, however you choose to write it.
Re: 88: is a proposition internal to the modal logic. It just means that is false in whatever world is currently under consideration. It’s the judgements “” or “” which would mean (as I am using them) that is false generically.
What I’m saying is that we do want it to be generically true that (at any world where is false and is true, it (vacuously) must be that we see a possible world where is true), but we do not want it to be generically true that (this would be the claim that at any world where is false and from which we see a possible world where is true, it must be the case that we see a possible world where is true).
Re: no post in particular: The possible worlds semantics should make everything mechanical to see: Take modal propositions to be implicitly indexed by a variable of some sort . So is really , for some free variable . Furthermore, there is also some “accessibility” binary relation on . The operator is defined by [that is, holds at a world just in case holds at every world accessible from there]. The operator is defined by [that is, holds at a world just in case holds at some world accessible from there].
That should make it clear what rules should, and should not, hold, just by turning the translation crank and considering familiar predicate logic. By default, this yields . Making reflexive and transitive gets . Making an equivalence relation gets .
Or perhaps it would be easier to think in terms of topological models of ; here, propositions amount to subsets of a topological space (there is no presumption that these be closed or open or what have you). Standard logical operators behave standardly. amounts to the claim that (of course, if there are multiple antecedents on the left side, they are implicitly conjoined). acts as interior, and acts as closure.
Note that, if is the empty set and is not closed, we have that (since will be the empty set) but we don’t have that (because will be nonempty).
Maybe I have too much internalized the type-theoretic notion that all rules should make sense in any context. But it’s hard for me to understand how logic can be practical otherwise. Of course, this is just the problem that we have with , so maybe I should get used to it…
Ah, sure. Ordinary logic has this “deduction theorem” property that if you can conclude from , then you can conclude (and, a fortiori, for arbitrary ). Modal logic scuttles that.
Do you at least see intuitively why we don’t want , though? Just because it’s possible that the Democrats will not win in 2016 (taking to be the proposition that the Democrats will win in 2016, this is , or just as well, for arbitrary ) and it’s possible that the Democrats will win in 2016 () doesn’t mean definitionally false things are possible () or that everything whatsoever is possible ( for arbitrary ).
To be honest, I’ve never been able to make much intuitive sense of what modal logicians mean by “possible” and “necessary”. (-:
Something to wonder about is how this base change idea works with types, including dependent ones. Let’s start with a type dependent on Worlds, such as . Then a possible team at world is a pair , where is accessible to and is a team in that world. I’ll take it that all worlds are accessible to each other. On the other hand, a necessary team at a world is a section, i.e., a function . So ’Team which finished eighth in ’ or a named team if it appears in every world. This is like my necessary ingredient of beef stew from this post, except maybe I wasn’t thinking of context extension back to back then.
These seem like different ways to pick out a section, one by a feature defined relative to the world, the other by some trans-world identifying name.
So then what happens if we have further dependency
Then a possible player at is a triple , with and , as I was trying to get at here.
What of a necessary player? From previous conversations we doubted it could be formed in just any context, so there shouldn’t be a notion of necessary player for a team in a world, but presumably it’s OK to have a function from the image of a necessary team to the players in those teams. For example, ’the youngest player in the team which finishes eighth’, or ’The captain of Manchester United’, if that team appears in every world. I suppose we could even name someone if they play in all worlds for a necessary named team.
What happens when Worlds belongs to a richer type theory, such as a cohesive one might be interesting. We’d have more of an idea of there being ways of making minor modifications to our world. So we can imagine counterparts to individuals in this world in near neighbouring worlds.
That distinction I pointed to above between a feature defining something relative to a world and a trans-world identifying name is at the heart of Kripke’s Naming and Necessity:
…proper names, in contrast to most descriptions, are rigid designators: A proper name refers to the named object in every possible world in which the object exists, while most descriptions designate different objects in different possible worlds. For example, ’Nixon’ refers to the same person in every possible world in which Nixon exists, while ’the person who won the United States presidential election of 1968’ could refer to Nixon, Humphrey, or others in different possible worlds. (Wikipedia)
So I guess a possible possible team at is a triple , where is accessible to , is accessible to and . Then with transitive accessibility relation (forced on us as we’re in the -groupoid business), projection to , is the map .
Necessary necessary Team next.
One of the reasons I’ve never been able to make much sense of modal logic is that I have no idea what it means for something to be “possibly possible”. Another is that I don’t really see how the meaning of “possibly” is at all explicated by saying that something is possible if it is true in some possible world. (-:
Yeah; as noted before, the words “necessary” and “possible” can be used in many different senses, and I think many of the ordinary language ways in which they are used do not actually give any significant sense to iterated modalities like “possibly possible”. I also share the feeling that there is a lack of explicatory power in translating ordinary language “possible” to “possible worlds”. But I would have to say that I’m not terribly concerned with using modal logic to shed light on metaphysical issues and the language around them anyway. Yet the formalism that happens to be called “possible worlds semantics” is a mathematical notion of some naturality which is interesting to contemplate, I think, and finds modelling applications that have nothing to do with necessity or possibility in any alethic sense. (In much the same way that I would tell people the formalisms which happen to be called “intuitionistic logic” can be interesting and useful to contemplate, even if one doesn’t care at all about Brouwer’s philosophy of mathematics or such things)
For example, one situation describable using modal logic is like so: imagine playing a turn-based game of some sort, in which, at various times, various things are or are not true (e.g., one might be playing chess, and considering propositions such as “Both queens are still on the board”, “White is in check”, “It is black’s turn”, “There is a knight on a5”, etc.). We might use to mean “Every move available will result in being true”, while using to mean “Some move available will result in being true”. This is a sort of “possible worlds” framework, where the “possible worlds” are game states, but one needn’t attach it any metaphysical significance; you’re just analyzing the game tree. The proposition “” in this context just means “There is some sequence of two moves which will result in ”. To assert a theorem such as “” (where is the proposition that no player has two bishops on squares of the same color) is just to note an invariant of the game. All the rules of modal logic are applicable here, but the interpretation doesn’t demand confronting any lofty philosophical issues.
Very nice example! Although I think isn’t actually true; couldn’t someone promote a pawn to a bishop? (-:
Ah, good point! I was glibly using the system (the base modal logic + the axiom “C’mon, just make it a queen and stop taunting me!”)… :)
There’s a whole slew of temporal logics with branching futures, dense orderings, and so on.
So we have to wait for directed HoTT before we can have a poset of worlds?