Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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

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

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

    There’s a classic debate which has run for the past century as to how to deal with a following situation presented by Russell in On Denoting. Consider the statements:

    • (i) King George knows that Scott is Scott
    • (ii) Scott is the author of Waverley
    • (iii) King George knows that the author of Waverley is Scott

    Famously (iii) is false since King George had to ask for this information, and yet it appears to result from substituting one term for the other in (ii) into (i).

    The ’X knows’ operator is often taken as modal. Two kinds of solution then developed:

    • (i) Restrict substitution of identicals to occur within simple (atomic) propositions, thereby excluding the occurrence of modalities;
    • (ii) Russell suggested that ‘the author of Waverley’ is not a term, so cannot be used to replace Scott.

    Given our analysis of the, it seems that we don’t want (ii).

    Looking to the larger picture, has it all been worked out about how path induction works in the situation of modal types?

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2014

    An even easier case looks at two names for what turns out to be the same person, traditionally Cicero and Tully. Then

    • X knows that Cicero is happy
    • Cicero is Tully
    • Therefore, X knows that Tully is happy

    is not valid. Have I got this right that we don’t have a construction

    • P:Type,c:P,t:P\vdash P: Type, c: P, t: P
    • x:PH(x):Propx: P \vdash H(x): Prop
    • a:H(c)\vdash a: \Box H(c)
    • p:Id P(c=t)\vdash p: Id_P(c = t)

    to produce a term in H(t) \Box H(t)?

    But with the corresponding possibility modality ’as far as X knows’, we do have

    • As far as X knows Cicero may be happy
    • Cicero is Tully
    • As far as X knows Tully may be happy

    because

    • a:H(c)\vdash a: \bigcirc H(c)
    • p:Id P(c=t)\vdash p: Id_P(c = t)

    does allow me to form a term in H(t)\bigcirc H(t)?

    • CommentRowNumber3.
    • CommentAuthorZhen Lin
    • CommentTimeMar 31st 2014

    That seems to suggest that \Box does not operate on dependent types, i.e. the rule

    x:PH(x):Propx:PH(x):Prop\frac{x : P \vdash H (x) : Prop}{x : P \vdash \Box H (x) : Prop}

    is not sound. If it were then we could use path induction (= indiscernibility of identicals) as usual.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2014

    It makes sense in the ’locally everywhere’ interpretation of \Box, such as in Awodey-Kishida sheaf semantics. A contingent identity in one world (one fiber) might not hold everywhere locally.

    Dependent types meets sheaf interpretation of modal logic would seem to need fibrations within a fibration.

    Is there something about acting somehow on each fiber of a fibration not yielding a fibration?

    • CommentRowNumber5.
    • CommentAuthorZhen Lin
    • CommentTimeMar 31st 2014

    I don’t see how that’s relevant. The assumption p:c=t\vdash p : c = t has empty context, so it holds everywhere.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2014

    Have you seen Awodey and Kishida’s paper? If sheaf semantics can be used for first-order modal logic, it’s not too much of stretch to think that something similar would work for modal dependent type theory. In their system, P\Box P holds at a world (point in the base space), if PP holds for all the worlds in a neighbourhood.

    My thought was that two terms that might designate the same individual in one world could differ in another. This is like the classic case:

    • Nixon = 37th President of the US
    • Necessarily, 37th President of the US was a president of the US
    • Not necessarily, Nixon was a president of the US.

    Metaphysicians illustrate this in terms of a close possible world to ours in which Nixon became a lawyer and didn’t enter politics.

    • CommentRowNumber7.
    • CommentAuthorZhen Lin
    • CommentTimeMar 31st 2014

    Let’s not bring natural language into this and stick with formal systems. You said,

    • P:Type,c:P,t:P\vdash P: Type, c: P, t: P
    • x:PH(x):Propx: P \vdash H(x): Prop
    • a:H(c)\vdash a: \Box H(c)
    • p:Id P(c=t)\vdash p: Id_P(c = t)

    and I say, if we admit the rule

    x:PH(x):Propx:PH(x):Prop\frac{x : P \vdash H (x) : Prop}{x : P \vdash \Box H (x) : Prop}

    then we can conclude, using the standard rules for dependent type theory with equality, that H(t)\vdash \Box H (t).

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2014
    • (edited Mar 31st 2014)

    Sure, I agree with that.

    I was thinking about reasons we might be motivated not to admit the rule

    x:PH(x):Propx:PH(x):Prop.\frac{x : P \vdash H (x) : Prop}{x : P \vdash \Box H (x) : Prop}.

    What happens with Urs’s comonad flat modality? Do we have

    x:PH(x):Typex:PH(x):Type?\frac{x : P \vdash H (x) : Type}{x : P \vdash \flat H (x) :Type}?

    Is this something to do with the point in Urs and Mike’s paper where they write

    One maybe tempted to define the coreflection \flat as we did the reflections \sharp and Π\Pi, but this would amount to asking for a pullback-stable system of coreflective subcategories of each H/X\mathbf{H}/X, and at present we do not know any way to obtain this in models.

    • CommentRowNumber9.
    • CommentAuthorZhen Lin
    • CommentTimeMar 31st 2014

    The issue is basically the same, yes. In isolation, the rule

    H:TypeH:Type\frac{\vdash H : Type}{\vdash \Box H : Type}

    only forces us to define \Box for non-dependent types; but in the presence of the weakening rule, we also get

    x:PH(x):Typex:PH(x):Type\frac{x : P \vdash H (x) : Type}{x : P \vdash \Box H (x) : Type}

    for every type PP, forcing us to define \Box for all dependent types, and the substitution rule (for judgemental equality) forces this to be pullback-stable.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 31st 2014

    It seems to me that what this argument shows is that the argument of “X knows” is not a type but a piece of syntax, i.e. it is “quoted”.

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 1st 2014

    Re Mike #10, I don’t quite see what you’re saying. As you know, there’s been a long tradition of taking certain constructions of the form “it is ??? that” as modalities attached to propositions, e.g, “it is necessarily the case that”, “it is known that”. You can at least see a family resemblance between them.

    Now, it could all be misguided trying to develop a modal logic to capture such constructions, but then you may find philosophers unhappy that you’ve taken the term to talk about truncations, flat, sharp, etc., with no bearing on the historical use of modality.

    Is there nothing to tell people pouring over puzzles such as:

    • 9 = the number of planets in the solar system
    • Necessarily, 9 is greater than 7
    • Not necessarily, the number of planets is greater than 7?
    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2014

    On reflection, I think that what I was (very poorly) attempting to say is roughly equivalent to what Zhen is trying to say. Of course a modal operator like “X knows that …” is, like any other connective or quantifier, an operation on syntax. My point was that the meaning of this syntax is not “truth-functional”, i.e. it is not internalizable as a map PropPropProp \to Prop, since there can be statements PP and QQ that are equivalent (i.e. equal as elements of PropProp), but such that “X knows that PP” is true while “X knows that QQ” is false. This is more or less equivalent to saying that we can’t apply it in a nonempty context, since on the one hand if we had a function :PropProp\Box:Prop\to Prop then we could just apply that function in any context, while on the other hand if we could apply \Box in any context then we could apply it to the variable xx in context x:Propx:Prop and then λ\lambda-abstract to get (λx.x):PropProp(\lambda x. \Box x):Prop\to Prop.

    This is indeed very much the same as the issue that Urs and I had with \flat, which we also weren’t able to internalize or apply in a nonempty context. In that case, we were able to sort of get around the issue by using the “externalized universe” Type\sharp Type; I wonder if something similar would be possible here?

    One issue is that I don’t know what it means to apply modalities like “X knows that” or “it is necessarily the case that” to a non-hprop type.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 1st 2014

    Traditionally, necessity reflects a stability under minor variation, where inessential features of an entity may alter, but essential features remain the same. So for an emerald, the property of being owned by me is inessential, but its being green is essential. This is often illustrated by ’possible’ world’ talk. The local neighbourhood approach of sheaf semantics for modal logic picks up on this idea. Close possible worlds to the ’actual world’ may have someone else own the gem, but it’s still green.

    Someone, Robert Brandom I think, once claimed that many kinds of entity named in our language already contain some modal aspect. Perhaps then we could say ’emerald’ is already modal with respect to necessity, ’necessarily an emerald’ and ’emerald’ being equivalent. Then some types would not be modal. So ’necessarily an ingredient of beef stew’ is not equivalent to ’ingredient of beef stew’, the choice to add some ale being contingent, where the choice of beef is not.

    But can’t we just ’guess’ how things might go by extending sheaf semantics to modal type theory? Awodey and Kishida look at untyped first-order modal logic, so have a set of individuals forming the domain of discourse, fibred over the possible worlds. Then a unary predicate picks out a subset of the total space. If an intensional type is modelled by an \infty-groupoid, is there a natural way to see this as a single fibre over a point in a base space of possible worlds?

    I was musing here that possible worlds could be taken themselves as forming a type, so that other types could depend on it.

    • CommentRowNumber14.
    • CommentAuthorZhen Lin
    • CommentTimeApr 1st 2014

    That’s a very different kettle of fish. We know how to work with well-behaved modalities (say, a Lawvere-Tierney topology), and we know how to extend the modal operator to non-propositional types in that case (namely, sheafification). The so-called “sheaf semantics” of Awodey and Kishida is not of this form. To put it in type-theoretic language, what they are doing involves two types, DD and XX, and their modal operator acts on DPropD \to Prop and XPropX \to Prop. You could do the obvious thing and replace PropProp with TypeType, but then I completely lose sight of what this is supposed to mean: why should we be considering types fibred over the “domain of discourse” DD?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2014

    Awodey-Kishida isn’t really what I would call “extending sheaf semantics to modal type theory”. I would say rather that they extend a classical semantics by a particular modality which happens to describe sheafification. In other words, they aren’t giving a sheaf-theoretic interpretation of modality; they’re giving a modal-logic interpretation of sheaves.

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 1st 2014

    Awodey-Kishida isn’t really what I would call “extending sheaf semantics to modal type theory”.

    I didn’t say it was. I meant, given what they did to classical logic, couldn’t we imagine doing something similar for dependent type theory?

    they aren’t giving a sheaf-theoretic interpretation of modality; they’re giving a modal-logic interpretation of sheaves.

    Hmm. Well, they’re not doing it for the benefit of helping mathematicians think about sheaves, rather to provide a complete semantics for a logic:

    In this paper the topological interpretation is extended in a natural way to arbitrary theories of full first-order logic. The resulting system of S4 first-order modal logic is complete with respect to such topological semantics.

    It’s an extension of the topological semantics for modal logic, as they say, in parallel with how Kripke sheaves are an extension of Kripke frames. And there’s a way of understanding the Kripke approach in terms of the topological approach.

    I believe his group have a generalisation, see Topos Semantics for Higher-Order Modal Logic:

    The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion.

    Why not homotopify?

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2014

    I meant, given what they did to classical logic, couldn’t we imagine doing something similar for dependent type theory?

    Ah, right. Sorry, I misunderstood what you were saying.

    I just went back to look at their paper again, and it looks like what they do depends fairly deeply on the traditional separation of “carrier sets” and “propositions” in first-order logic. In particular, they require the domains of variables to be sheaves and the basic function symbols to be continuous (i.e. maps of sheaves), but they allow relation symbols to be interpreted by arbitrary subsets (not necessarily subsheaves). I think this is what enables them to interpret \Box as “interior” in a way that’s stable under substitution.

    From a category-theoretic perspective, they’re considering the surjection of topoi Set XSh(X)Set^X \to Sh(X), where XX is a set equipped with a topology, and the induced lex comonad GG on Set XSet^X. Then they interpret the types of FOL by GG-coalgebras and the terms by GG-maps, but the relations by subobjects in Set XSet^X that are not necessarily GG-coalgebras. Then if RDR \rightarrowtail D is such a relation, R\Box R is probably the pullback of GRGDG R \rightarrowtail G D along the GG-coalgebra structure DGDD \to G D.

    The natural generalization to DTT would be to consider GG itself as a “modal operator” on Set XSet^X. But then we run into the same problem that Urs and I had with \flat: it doesn’t internalize as an endomap of the universe, or act on dependent types in a substitutive way.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2014

    I haven’t been following in any detail (no time), but I see one thread that we keep re-hashing. Just to highlight:

    David says something like this: There is all this traditional study of modal logic, and now here we are suddenly talking about a bunch of modalities in (homotopy) type theory without connecting to this traditional theory. Shouldn’t one make the connection?

    (Is that roughly an accurate paraphrase, David?)

    One impression about the traditional theory that I have is that its translation to English language modalities such as “necessity” tends to be artificial and driven more by the wish to make an identification than by an actual argument that the identification makes sense. As a result one runs into puzzlements of the kind that David highlights above. (Beyond the initial puzzlement of why a necessary truth should be “necessarily necessary”, as the usual phrasing of S4 in English language suggests. )

    It seems to me that to make good sense of modalities of the kind “is known to be true” would require a vastly elaborate axiomatic system that would have actual reflection of complex concepts such as “knowledge”. I can see why philosophers are interested in this, but it just seems far premature to try (or pretend to) actually formalize this.

    Personally I feel that the more “technical” and less “complex” modalities that we discuss in modal type theory (such as “is discrete”, “is codiscrete”) give a much better sense of what formal modality really is and can achieve.

    • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 2nd 2014

    …a much better sense of what formal modality really is and can achieve.

    That would a difficult message to sell to my colleagues. I’m sure they’d think we’d just changed the subject. You’d be surprised at the extent to which ’possible world’ talk has become second nature to many in philosophy departments.

    Perhaps we could say there are three attitudes to take here about ’philosophical’ motivation:

    A) That the aim should be to get to the bottom of the nature of modalities, one of the most important of which is metaphysical necessity.

    B) That it’s possible that thinking about such things can inspire some interesting developments in logic and mathematics.

    C) That it’s largely a distraction and that one should follow the mathematics.

    That Kripke adopted (A) is clear. Read ’Naming and Necessity’ and you see him grapple with the metaphysics of possible worlds. Or consider the description of a recent book by one of the UK’s most prominent philosophers.

    I’m more inclined to (B). Even if Kripke was motivated in (A) style, it inspired him to develop Kripke frame semantics, a useful logico-mathematical idea. On a different topic, had we thought about Russell’s treatment of definite descriptions earlier (The King of France is bald) and tried to understand it type theoretically, we might have been led, before the rise of HoTT, to the need for a notion of contractability. So looking to see if anyone’s thought about modalities applied to types might pay off in unexpected ways.

    But I’m also led by (C) considerations, in particular here the idea that there might be a way to take an existing classical set-up and extend it to a dependent type-theoretic one. So there’s an idea that bolted onto some Stone-like duality between Theories and their Models, one can take Modal Theories as the algebras for some monad and Modal Models as the the coalgebras for a comonad. The latter has the effect of turning a semantics into a frame semantics. Maybe something similar is possible on top of a Stone-like duality between HoTTs and their models.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeApr 2nd 2014
    • (edited Apr 2nd 2014)

    Interesting you mention that Kripke was fascinated by a “metaphysics of possible worlds”. He would be very much in the fashion these days, too.

    But what kind of worlds are we going to capture with formalism? Worlds that usefully contain the king of France will be hard to capture, accordingly formal reasoning about them is out of reach.

    But I suppose I get the point now. I guess you’d want to be talking assuming some theory has been specified, and then have formal statements about aspects of its models. Some will be theorems of the theory, hence will necessarily hold in all models. Some will hold only in some models. If they hold in at least one model, then they are possibly true.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeApr 2nd 2014

    If that last suggestion is right, or is adopted, then that would mean that given a type of models over a theory, the necessity modality should be the monad on the category of types dependent on that type of models which is induced by dependent product, possibility would similarly be the comonad induced by dependent sum. Does that resonate with anything that modal people consider?

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeApr 2nd 2014

    Urs 18 sounds like you are imagining (although I doubt that you actually think this) that someone invented the formal theory of modalities first and then started trying to translate them into ordinary language and came up with ideas like “possiby”. I’m sure the situation is the reverse: people wanted to describe language like “possibly” and invented formal modalities in order to do it. One can argue about how successful they were, but I expect to a philosopher that’s the point of the whole subject.

    I don’t see any a priori reason why making sense of (say) epistemic modalities must require a vastly elaborate system of axioms about knowledge, any more than making sense of cohesive modalities requires a vastly elaborate description of topological groupoids. Even if constructing the semantics is complex, the syntax can be simple.

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeApr 2nd 2014

    I think the “\Box doesn’t act on dependent types” point of view would reply to #11 as follows. The equality “9 = the number of planets in the solar system” is in the identity type of \mathbb{N}. We’d like to transport along this equality in a dependent type (x:)(x>7)type(x:\mathbb{N})\vdash \Box(x\gt 7)\, type, but there is no such dependent type; the best we can hope to get from (x:)(x>7)type(x:\mathbb{N})\vdash (x\gt 7) \,type is (x:)(x>7)type(x:\Box\mathbb{N})\vdash \Box(x\gt 7)\, type.

    So what is \Box\mathbb{N}? It’s natural to pronounce it as “the type of necessary natural numbers”. In #13 you suggested that some types are already modal, and if all emeralds are necessarily emeralds, it seems that all natural numbers would also be necessarily natural numbers. But even if that’s the case (which I’m not sure of), I think it would only argue that the counit map \Box \mathbb{N} \to \mathbb{N} is surjective. It might be the case that two necessary natural numbers have equal underlying natural numbers, but are not equal as necessary natural numbers, and that could be what’s happening here: 9 and “the number of planets in the solar system” are not necessarily equal, so we don’t have an equality in \Box \mathbb{N} to transport along in the dependent type (x:)(x>7)type(x:\Box\mathbb{N})\vdash \Box(x\gt 7) \,type.

    (I don’t quite understand the distinction that the syntax suggests between “equal as necessary natural numbers” and “necessarily equal as natural numbers”, though.)

    Similarly, we have “Scott = the author of Waverley” as an equality in the type PersonPerson, but it might not lift to an equality in the type Person\Box Person of “King George knows that PersonPerson”. We might interpret the latter as “King George’s mental model of the people in the world”, which could both omit some people that King George doesn’t know about, and include duplicate entries for some names that King George doesn’t realize refer to the same person. (It seems that it might also in theory contain fictitious people that King George believes in, which is a problem for defining a counit map PersonPerson\Box Person \to Person.)

    It’s less clear to me what happens when we transport the “planets” puzzle along the classical equivalence =¬¬\Box = \neg\diamond\neg, since the “possibility” modality \diamond is “monadic” and so one might expect to be able to apply it dependently. Perhaps it hinges on the interpretation of \diamond\mathbb{N}. Is it the type of all natural numbers that might possibly exist? If we have two terms of type \mathbb{N} which happen to be equal, but it is possible that they are unequal, what happens when we apply the unit map \mathbb{N} \to \diamond \mathbb{N}? I feel like perhaps this map is problematic in general and should be only a total relation.

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 2nd 2014

    In a snatched moment, re #23

    It seems that it might also in theory contain fictitious people that King George believes in

    “It is believed that” is generally taken not to satisfy S4. “It is known that” is generally taken to be something more or less approximated by “It is a justified true belief that”, so in particular requires truth. In which case we would not include fictitious people.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeApr 2nd 2014

    Got it, thanks.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeApr 2nd 2014
    • (edited Apr 2nd 2014)

    re #22: Maybe you might remind me, what is the reasoning that \Box should translate as “necessarily” and \bigcirc as “possibly”?

    What confuses me is that the axioms are just that of a plain (co-)monad on a poset, so arguing that this encodes specifically necessity and possibility says that no other modality will have a (co)monadic appearance (for if it did, it would be either necessity or possibility).

    I am really confused about this. I don’t want to be argumentative. I will shut up as soon as somebody explains it to me.

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeApr 2nd 2014

    re #19:

    just to remind myself I have created Naming and Necessity and cross-linked with a brief comment in the “Related concepts”-sections of both modal logic and multiverse.

    • CommentRowNumber28.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 2nd 2014

    Re #26, modal logicians need not restrict themselves to necessity/possibility. They are many modalities, including tense operators (’It will always be the case that’). Then there’s a vast range of possible modal logics (e.g., T, K, S1,…, S5, S4.5, etc.) (See here.) People argue as to which logic best captures which modality.

    Naturally there’s a complicated story to be told of how modal logic came to take the form it has. There’s an interesting SEP article Modern Origins of Modal Logic which shows that part of the story involves concerns about the difference between material implication and strict implication. Godel later gets involved relating intuitionistic to modal logic. This is not surprising as one interpretation of ’necessity’ is ’it can be proved that’.

    I should try to find out when ’metaphysical necessity’ gets taken seriously. One part of this story is that the logical positivists, who as positivists naturally wished to avoid metaphysics, had to come to terms with the difference between what appeared to be lawlike universal generalisations, and contingent ones, e.g.,

    • All planets move in ellipses
    • All coins in my pocket are silver

    They tried to do this by means of the linguistic form of the statements, but it was widely considered not to work. There seems something ’modal’ going on in the former. Throw in another planet and it moves in an ellipse; put a coin in my pocket and it might be copper.

    Kripke breaks with mere linguistic analysis to suggest we must talk about the world and the way it might be.

    I added a page for Carnap’s Meaning and Necessity.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeApr 2nd 2014

    so arguing that this encodes specifically necessity and possibility says that no other modality will have a (co)monadic appearance (for if it did, it would be either necessity or possibility).

    No, I think the point is that necessity and possibility are particular (co)monads, just as (say) an open subtopos, or the sharp modality, is a particular monad. The general framework of (co)monadic modalities includes all of them, but each presumably has specific properties and intended semantics not shared by the others.

    • CommentRowNumber30.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 3rd 2014

    Re #29, yes, not forgetting that modal logicians work in systems weaker than S4, so not even monadic. Some hold that S4 doesn’t hold even for necessity, e.g., here.

  1. Here is somewhat related comment on modal operators in topos theory. Let \mathcal{E} be a topos and jj a Lawvere-Tierney topology in \mathcal{E}. This is a morphism j:ΩΩj : \Omega \to \Omega; for any formula φ\varphi of the internal language of \mathcal{E}, one obtains a weakened formula j(φ)j(\varphi), where the precise meaning of “weakening” depends on the topology in question.

    The association φj(φ)\varphi \mapsto j(\varphi) is truth-functional, so the interesting philosophical puzzle mentioned in #1 does not apply here.

    However, one can also define the jj-translation φφ j\varphi \mapsto \varphi^j. Like the double negation translation, this is obtained by putting a jj in front of every subformula. (The meaning of φ j\varphi^j is that φ\varphi holds on the subtopos Sh j()\mathrm{Sh}_j(\mathcal{E}) of jj-sheaves, i.e. φ j\mathcal{E} \models \varphi^j if and only if Sh j()φ\mathrm{Sh}_j(\mathcal{E}) \models \varphi.)

    There is then the following observation: Let φ\varphi and ψ\psi be two formulas which happen to be equivalent in \mathcal{E}. Then it is not necessarily true that φ j\varphi^j and ψ j\psi^j are equivalent as well. However, if there is an intuitionistic proof of φψ\varphi \Leftrightarrow \psi (which in particular implies that φ\varphi and ψ\psi are equivalent in \mathcal{E}), then the jj-translated formulas are equivalent as well: φ jψ j\varphi^j \Leftrightarrow \psi^j.

    In the example of #1, there is no intuitionistic proof that Scott is the author of Waverly (this simply happens to be true), so the equivalence “Scott is Scott \Leftrightarrow the author of Waverly is Scott” is not preserved when applying a jj-translation.

    • CommentRowNumber32.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 11th 2014
    • (edited May 11th 2014)

    Revisiting this thread, Mike in #23 wrote

    It’s less clear to me what happens when we transport the “planets” puzzle along the classical equivalence =¬¬\Box = \neg\diamond\neg,…

    One thought is that in grafting on modalities to some type theory, we might start by extending intuitionistic modal logic rather than the classical variety. In propositional versions of the former, \Box and \diamond are independent. It seems there is an IntK \mathbf{IntK}_{\Box \Diamond}, which has \Box operating on conjunctions as you’d expect, and likewise \diamond on disjunctions. Then there’s IK\mathbf{IK} which adds connecting axioms:

    • (ϕψ)(ϕψ)\diamond(\phi \to \psi) \to (\Box\phi \to \diamond\psi)
    • (ϕψ)(ϕψ)(\diamond\phi \to \Box\psi) \to \Box(\phi \to \psi)
    • CommentRowNumber33.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 12th 2014

    IS4\mathbf{IS4} then adds in axioms to ensure that \Box is a comonad and \diamond a monad. So it seems any interaction between a pair of modalities happens through those connecting axioms above. Can they be seen as arising from some category theoretic construction?

    • CommentRowNumber34.
    • CommentAuthorTim_Porter
    • CommentTimeMay 12th 2014
    • (edited May 12th 2014)

    Is the paper by Eric Goubault and his brother relevant here? I sort of remember their use of intuitionistic S4 (in one of its forms) and then modelling it by simplicial sets. It was: On the Geometry of Intuitionistic S4 Proofs, published in “Homomogy, Homotopy and Applications” (2003) and is linked to from Eric Goubault’s homepage.

    • CommentRowNumber35.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 12th 2014

    According to Characterising intermediate tense logics in terms of Galois connections, it’s better to see the connecting axioms of #32 as mediating between a pair of galois connections to form a tense logic, i.e. one with four operators

    FAF A (AA is true at some future time), PAP A (AA was true at some past time), GAG A (AA will be true at all future times), and HAH A (AA has always been true in the past).

    Of course, Galois connections are a promising direction if we want to find pairs of modalities as adjoints in an adjoint cylinder.

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2014

    Oh, wow, I hadn’t been aware that anyone discussed adjoint modalities in the context of Galois connections, as on the bottom of p. 3 of the article (arXiv:1401.7646) that you mention.

    I need to chase those references…

    • CommentRowNumber37.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 12th 2014

    The ones I’ve seen have all taken comonadic modalities only to be right adjoints, e.g., Hermida in A categorical outlook on relational modalities and simulations. I guess that result at the top of p. 11 is closely related to the paper of #35’s entwined pairs of tense operators.

    • CommentRowNumber38.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 5th 2015

    Returning to Mike’s #23, with the base change idea from necesssity and possibility, we see now we want \Box to take world-dependent types to world-dependent types, that is, the sections extended back to WW.

    The constants 7(w),9(w):N(w)7(w), 9(w) : \Box N(w) and also Thenumberofplanets(w):N(w)The number of planets(w): \Box N(w).

    Then we may have 9(a)=Thenumberofplanets(a):N(a)9(a) = The number of planets(a): N(a), but 9(w)Thenumberofplanets(w):N(w)9(w) \neq The number of planets(w): \Box N(w).

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2015
    • (edited Jan 5th 2015)

    I see what you and Mike are getting at here, but I don’t quite see yet how what you write will actually do what it’s intended to. Maybe I am missing something, but while that is so, allow me to suggest that it works as follows:

    Given any type WW let WH /W\mathbb{N}_W \in \mathbf{H}_{/W} be the constant \mathbb{N}-bundle, i.e. W=(W×p 1W)\mathbb{N}_W = (W \times \mathbb{N}\stackrel{p_1}{\to} W).

    Then the difference between 9: W9 \colon \mathbb{N}_W and NumberOfPlanetsInSolarSystem: WNumberOfPlanetsInSolarSystem \colon \mathbb{N}_W is that 99 is a constant section of the constant bundle (taking the same value on all wWw \in W) while NumberOfPlanetsInSolarSystemNumberOfPlanetsInSolarSystem is not a constant section.

    (Has it ever been mentioned in this thread here that indeed in our particular world the number of planets in the solar system is not 9? )

    So they are of the same type, the difference you are after is elsewhere:

    Consider the squashed identity type [x=y][x = y] for simplicity (i.e. the proposition which is the (-1)-truncation of the identity type). Then consider the WW-dependent type

    [9=NumberOfPlanetsInSolarSystem][9 = NumberOfPlanetsInSolarSystem]

    This is a bundle of propositions over WW. Its fiber over wWw \in W is the unit type if NumberOfPlanetsInSolarSystem(w)NumberOfPlanetsInSolarSystem(w) is 9, otherwise it is the empty type.

    So the W-dependent type [9=NumberOfPlanetsInSolarSystem][9 = NumberOfPlanetsInSolarSystem] is not inhabited. In other words for W=W * W\Box_W = W^\ast \prod_W we have W[9=NumberOfPlanetsInSolarSystem]=False W\Box_W [9 = NumberOfPlanetsInSolarSystem] = False_W (where False WFalse_W is the W-dependent proposition which is false for all wWw\in W), which we read as: “It is false that it is necessary that the number of planets in the solar system is 9.”, just as it should be.

    However, with W=W * W\lozenge_W = W^\ast \sum_W we have W[9=NumberOfPlanetsInSolarSystem]\lozenge_W [9 = NumberOfPlanetsInSolarSystem] is an inhabited WW-dependent type. This we read as “It is true that it is possible that the number of planets in the solar system is 9.”, just as it should be.

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2015

    I have taken the liberty of adding that to necessity and possibility – Examples.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeJan 6th 2015

    So, really, the possible-worlds-modal-logic reply to #11 is that “9 = the number of planets in the solar system” can’t be asserted in the empty context; only necessary truths can be asserted in the empty context. (As always, it seems unsatisfying that the possible-worlds semantics doesn’t do anything to distinguish this world from all the other possible ones.)

    • CommentRowNumber42.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 6th 2015
    • (edited Jan 6th 2015)

    Re #39, that’s the proper rendering of what I was gesturing at. I’m afraid the number 9 is just a vestige from earlier, happier days for Pluto in the Kripkean past.

    Re #40, without wishing to open up that discussion, could we not send the S4 discussion on necessity and possibility elsewhere. Maybe to the logic S4(m)? Perhaps we could rename to ’necessity and possibility in HOTT’, or some such title, to discourage it becoming a place for other topics.

    Re #41, can’t I write

    a:W\vdash a:W

    9(a)=thenumberofplanetsinthesolarsystem(a)\vdash 9(a) = the number of planets in the solar system(a)?

    We then have reassuringly

    [NumberOfPlanetsInSolarSystem=9](a)\Box [Number Of Planets In Solar System = 9](a) implies [NumberOfPlanetsInSolarSystem=9](a)[Number Of Planets In Solar System = 9](a) implies [NumberOfPlanetsInSolarSystem=9](a)\lozenge [Number Of Planets In Solar System = 9](a).

    Of course, there’s still work to be done even to form ’thesolarsystem(w)the solar system(w)’. It relies on there being a contractible WW-dependent type solarsystem(w)solar system(w). If at least Sol(w):Star(w)Sol(w): \Box Star(w) were a ’rigid designator’, and we had a dependent type ’planets of star(s)’, then something could be done. Of course, the complications of astronomy start to kick in with rogue planets, and binary stars with no planets , etc.

    With Sol(w)Sol(w) we meet the counterparts/rigid designator debate that was often phrased in terms of ’Nixon’. Either I use a phrase which characterised Nixon in this world and might be thought to designate an individual in all possible worlds, such as ’the 36th president of the US’ (generating its own transworld issues) and seemingly not indicating the ’essence’ of Nixon, or I claim it is possible to pick out counterparts to Nixon in other worlds. You may imagine what there is to be said on the subject, e.g., in a very close world a different sperm reached a different egg, etc.

    • CommentRowNumber43.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 6th 2015
    • (edited Jan 6th 2015)

    I can see that my N(w)\Box N(w) from #38 didn’t look like it, but I did intend what Urs would have in #39 as W W\Box_W \mathbb{N}_W.

    But then why do you have NumberOfPlanetsInSolarSystem: WNumberOfPlanetsInSolarSystem \colon \mathbb{N}_W and not NumberOfPlanetsInSolarSystem: W WNumberOfPlanetsInSolarSystem \colon \Box_W \mathbb{N}_W? Surely you want it to be a section, and then extended back to WW.

    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2015
    • (edited Jan 6th 2015)

    Mike, re #41, how about if we say it like this:

    A necessity modality \Box is always attached to a given choice of context/slice over WW – and should therefore better always be subscripted as W\Box_W – but with that understood, then it is indeed an endofunction on the type universe, but on the type universe in the slice of WW, i.e. it is a function W:Type WType W\Box_W : Type_W \to Type_W . (Hm, is that right? Or something like this.)

    David, re #43,

    But then why do you have NumberOfPlanetsInSolarSystem: WNumberOfPlanetsInSolarSystem \colon \mathbb{N}_W and not NumberOfPlanetsInSolarSystem: W WNumberOfPlanetsInSolarSystem \colon \Box_W \mathbb{N}_W? Surely you want it to be a section, and then extended back to WW.

    Here I am not sure what you are after, as the term NumberOfPlanetsInSolarSystem: WNumberOfPlanetsInSolarSystem \colon \mathbb{N}_W already is a section (of p 1:W×Wp_1 : W \times \mathbb{N} \to W). Its categorical semantics is a horizontal map in

    W NumberOfPlantesInSolarSystem W× id p 1 W \array{ W && \stackrel{NumberOfPlantesInSolarSystem}{\longrightarrow} && W \times \mathbb{N} \\ & {}_{\mathllap{id}}\searrow && \swarrow_{\mathrlap{p_1}} \\ && W }

    and this seems to do just what it’s supposed to.

    • CommentRowNumber45.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 6th 2015

    Maybe starting with a non-dependent type such as \mathbb{N} isn’t helping since we need W *W^\ast to even start, but what I’m really interested in is your W:Type WType W\Box_W : Type_W \to Type_W applied to general types not just propositions.

    So let’s see what happens through the steps of applying W=W * W\Box_W = W^\ast \prod_W to W *W^\ast \mathbb{N}.

    WW *\prod_W W^\ast \mathbb{N} is just the non-dependent type [W,][W, \mathbb{N}].

    Extending back under W *W^\ast, then gives us pairs w,f\langle w, f \rangle fibred over the first component, where f:[W,]f: [W, \mathbb{N}].

    So this is WW *\Box_W W^\ast \mathbb{N}, a world-dependent type, and at my world (and so at any world), the functions ’9’ and ’number of planets’ aren’t the same, even if evaluated at my world they give the same answer.

    Maybe since we started with an extension, this seems less motivated. Let’s pick a more interesting world-dependent type such as CB(w)CB(w) for celestial bodies in universe ww. What happens if we apply W\Box_W to it? Again we have pairs w,f\langle w, f \rangle, where ff takes a world to a celestial body of that world. Two such ffs are ’The evening star’ and ’The morning star’ (assume all universes have something unique that brightly shines at the right time). Assuming also that in some universe they differ, we have that ’The evening star’ and ’The morning star’ are not identical.

    Of course, this is already true back over in the non-sliced situation, but since we’re looking at modalities as maps from slice over WW to itself, we can also say that w,morningstar\langle w, morning star \rangle and w,eveningstar\langle w, evening star \rangle are not identical, so express the situation as a non-identity in WCB(w)\Box_W CB(w).

    Does that make sense?

    • CommentRowNumber46.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 6th 2015

    Of course, we can also do it your way and reduce to a world-dependent proposition ’morning star(w) = evening star(w)’, but my point is that we don’t have to restrict ourselves to propositions when applying modalities.

    • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2015

    I didn’t mean to suggest to concentrate only on dependent propositions. That just seemed to be the thing to do in the example at hand.

    I agree with all you say above. I am just wondering what you have in mind where you say “isn’t helping”. Do you want to exclude explicitly applying W *W^\ast?

    The W *W^\ast-operation (maybe we should find a nicer symbol for it) has the nice feature that it captures the idea, mentioned in the above discussion, of “necessary terms”.

    A term might be called necessary (or rather “WW-necessary”) precisely it is in the image under W *W^\ast of a global term.

    Maybe it’s possible to characterize the WW-necessary terms by just using WW * W\Box_W \coloneqq W^\ast \prod_W and not W *W^\ast itself? Hm, not sure.

    • CommentRowNumber48.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 6th 2015

    By “isn’t helping”, I just meant “is making harder to see what’s going on”. But in fact working through the CB example, it didn’t make much of a difference.

    All it seemed to boil down to in the question of whether to work here with necessity applied to all types rather than just propositions was something like the difference between being able to say straight out of two functions that they’re different, and only being able to express this in terms of a place where they differ.

    A term might be called necessary

    Do we need to give a condition for when a term should be called necessary? Doesn’t a term always come as typed, in which case if its typed by a WW-necessary type, then it’s WW-necessary.

    But then what is a WW-necessary type? Something in the image of W\Box_W? We don’t have idempotency, but maybe that doesn’t matter.

    The two things I see as needing doing are

    1) To engage with philosophers, one would need to have thoughts on the Nixon/counterparts issues I mentioned in #42.

    2) See what happens for more interesting WWs than discrete sets.

    i) We already spoke once of allowing it to be BG\mathbf{B} G. I had an inkling it might be possible to tie in with what people were saying about perceptual invariants.

    ii) Then there could be cohesive world types, etc. When Judea Pearl takes up Lewis’s account of possible worlds to approach counterfactuals, he uses a notion of proximity of worlds in terms of certain minimal changes to make it the case that AA, when we say had AA been the case, BB would have happened.

    • CommentRowNumber49.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2015
    • (edited Jan 6th 2015)

    Whether “necessary term” is a good English word to choose here may be debatable, I was just suggesting that reading it as “constant term” comes close to how you and Mike seemed to have imagined using it above.

    A term of type WX\Box_W X does not need to be constant (while the type WX\Box_W X is constant) so calling these terms “necessary terms” would be an incompatible convention. I’d rather call terms of WX\Box_W X “witnesses of necessity”, and there may be a different witness in different worlds.

    I am all in favor of discussing this for the case that W=BGW = \mathbf{B}G. I keep trying to advertize to HoTT-practitioners that working with HoTT in the context of pointed connected types has the enormous potential of being a synthetic version of homotopy representation theory. Would seem to be a most excellent topic for everyone looking for topics in HoTT. But so far nothing much has happened. (Generally, presently nothing much seems to be happening on the HoTT-front?!)

    • CommentRowNumber50.
    • CommentAuthorMike Shulman
    • CommentTimeJan 6th 2015

    A necessity modality \Box is always attached to a given choice of context/slice over WW – and should therefore better always be subscripted as W\Box_W – but with that understood, then it is indeed an endofunction on the type universe, but on the type universe in the slice of WW, i.e. it is a function W:Type WType W\Box_W : Type_W \to Type_W.

    Yes, I agree. What I’m getting out of this discussion is that maybe WW *Π W\Box_W \coloneqq W^* \Pi_W doesn’t really deserve to be called “necessity” when applied to non-propositions. A term of W\Box_W \mathbb{N}, as David said, consists of, for each world, a function assigning a natural number to every world. (I don’t think it’s necessary to write W\mathbb{N}_W, since this is in fact the natural numbers object in the slice over WW.) It’s not clear to me what is “necessary” about this. One might be tempted to say that an element of W\Box_W \mathbb{N} is “a natural number that exists in all worlds”, but in fact that’s already true of elements of \mathbb{N} itself as long as we are in the slice over WW. The same is true of CBCB; “The morning star” and “The evening star” are already both elements of CBCB. The difference between CBCB and WCB\Box_W CB is that an element of CBCB is a single function assigning to each world a celestial body in that world, while an element of WCB\Box_W CB consists of one such function for each world.

    • CommentRowNumber51.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2015
    • (edited Jan 6th 2015)

    So in homotopy type theory “necessarily” is to W\Box_W similar as W\exists_W is to W\sum_W: strictly speaking the former comes from the latter by composition with (-1)-truncation. It’s something to stay aware of, but is not troublesome, I’d say. Sometimes it’s useful to think of the untruncated W\sum_W as being “the real existential quantifier”, and maybe from some higher perspective the analog is true of W\Box_W, too.

    • CommentRowNumber52.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 6th 2015

    Re #50, but I guess at least instantiating WCB\Box_W CB at our actual world aa gives us a way to talk about a full function, such as Theeveningstar(w)The evening star(w) as fully existing for us in our world, if you see what I mean.

    So we get a nice map WCB(a)CB(a)\Box_W CB(a) \to CB(a).

    • CommentRowNumber53.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2015

    Although “instantiating at a world” isn’t something that takes place in the modal logic on which W\Box_W acts, but is an external or metatheoretic operation.

    • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015

    Coming back to the suggested terminology of “necessary types”: if we had an idempotent adjunction, then we’d immediately be justified to call X\Box X a \Box-type. Now the \Box we are looking at is not in general idempotent, but (assuming an ambient topos) it always factors through an idempotent operation (as here).

    Hm, on the other hand, how does that factorization of monads through idempotent monads interact with adjoints of monads. When does an adjoint triple factor through an adjoint cylinder?

    (This is slight abuse of terminology: Lawvere defined an adjoint cylonder to be an adjoint triple where the two outer adjoints are fully faithful, whereas here I am after the case where the middle one is.)

    • CommentRowNumber55.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015
    • (edited Jan 9th 2015)

    More concretely:

    given a morphism f:ABf \colon A \longrightarrow B in a topos H\mathbf{H}, what is the co-localization of H /X\mathbf{H}_{/X} at the f\prod_f-equivalences?

    The colocalization exists, and it does contain at least the objects in the image of the pullback f *()f^\ast(-), because (of course) for hMor(H /X)h \in Mor(\mathbf{H}_{/X}) a f\prod_f-equivalence then Hom(f *X,h)Hom(X,Prod f)Hom(f^\ast X, h) \simeq Hom(X, \Prod_f ) is an equivalence. So in this sense the objects of the form f *()f^\ast (-) really are “necessary types” (the ff-necessary types).

    Are there more necessary types?

    • CommentRowNumber56.
    • CommentAuthorMike Shulman
    • CommentTimeJan 9th 2015

    I didn’t follow why we know the colocalization exists. Is it because the idempotent comonad-core exists? Do we know that in the \infty-case?

    • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015

    I was thinking:

    First, a sufficient condition for Bousfield co-localizations of model categories to exist is their right properness. I take this from p. 9 of arXiv:0708.3435.

    This is for small sets of localizing morphisms, but I was assuming now that the resolution of the size issue is as for the known cases. But maybe I am wrong about that.

    • CommentRowNumber58.
    • CommentAuthorMike Shulman
    • CommentTimeJan 9th 2015

    Actually, it seems that Barwick’s condition is additionally for small sets of localizing objects. And it’s not clear to me that the usual sort of local-presentability tricks can be played to make large things small, since we are in the dual situation.

    • CommentRowNumber59.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015

    Thanks, good point. So I should take that back. Still we may ask for the class of co-local objects, which is maybe all that actually matters for the above discussion. It contains the objects in the image of f *()f^\ast(-) and what else?