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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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 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).

nLab > Latest Changes: S5 modal logic

Bottom of Page

1 to 17 of 17

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJul 26th 2023
    • (edited Jul 26th 2023)

    An elementary question, which may just show my ignorance:

    Given a pair of endofunctors □\Box, ◊\lozenge equipped with natural transformations of the form

    □⟶ε □id\Box \overset{\epsilon^{\Box}}{\longrightarrow} id

    and

    id⟶η ◊◊ id \overset{\eta^{\lozenge}}{\longrightarrow} \lozenge

    one can form a “combined naturality hexagon”, as shown here.

    This kind of hexagon seems to deserve a name. Does it have an established name? Is there a general notion that this is an example of?

    diff, v4, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJul 26th 2023

    added pointer to what I gather is the origin of the terminology “S5”:

    diff, v5, current

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeAug 1st 2023
    • (edited Aug 1st 2023)

    added a paragraph (here) making explicit the observation that S5 possible world semantics is exactly that induced by the base change adjoint triple along the quotient coprojection of S5 Kripke frames.

    diff, v13, current

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 2nd 2023

    Philosophers frequently now take propositions to be subsets of worlds. So rather than

    P:W→Prop, P: W \to Prop,

    they would take that PP itself to be a proposition, i.e., a map from WW to truth values.

    No big difference. We might say that PP is a WW-dependent proposition. But it does incline them to see only one fixed locus of variation, rather than treat WW as itself a variable.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeAug 2nd 2023

    This is classically the same thing: PropProp is classically the set of truth values and P:W→PropP \colon W \to Prop is a proposition about the elements of WW.

    Incidentally, I haven’t seen any literature phrasing it this way (either way): The modal logic texts that I have seen all insist on clunky notation encoding these proposition by their “valuations”. I have tried to streamline/modernize this a little.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 2nd 2023

    It goes back a long way, I think. In Are propositions sets of possible worlds?, Hoffmann attributes it to Stalnaker 1976. This turns out to be

    Stalnaker, R. 1976. Possible worlds. In Nous, 65-75. vol. 10. Revised version in his Inquiry, (1984) 43-58. Cambridge, MA: The MIT Press and in his Ways a World Might Be, (2003) 25-39. Oxford: Oxford University Press.

    The original is available

    I shall argue that the particular reduction that Adams proposes-a reduction of possible worlds to propositions-by itself says nothing that answers the critic who finds the concept of a possible world obscure. His reduction says no more, and in fact says less, about propositions and possible worlds than the reverse analysis that I would defend-the analysis of propositions in terms of possible worlds. (p. 71)

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeAug 2nd 2023

    Thanks. Looking over this it seems to be a re-hash of something much older still, the identification of propositions with subobjects.

    (I suspect this must be from the 1960s at least, though in checking our entry of subobject classifier I see that the first reference it gives is from 1970.)

    In any case I am not sure what you are saying in #4: There you say “rather than”, apparently meaning to contrast with something I wrote, but I don’t see the contradistinction.

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 2nd 2023

    I was pointing out that many philosophers will be confused with the formulation P:W→PropP: W \to Prop since for (many of) them, Prop=[W,2]Prop = [W, 2]. A proposition is just a predicate on worlds.

    They’ll think you’re writing P:W→[W,2]P: W \to [W, 2].

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeAug 2nd 2023

    The notation is standard and used, for what it’s worth, all over the nLab (starting with Prop).

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 2nd 2023

    I wasn’t suggesting we should change what we do here.

    But if ever you get invited to present to philosophers on this area, you may get some quizzical looks.

    I’m also formulating for myself what I think they struggle with concerning dependent type theory. They’re generally taking variation to be something that happens over a single special domain. So in first-order logic, it’s over a domain of everything. In propositional modal logic, it’s over a domain of worlds. First-order modal logic then becomes tricky for them because they either want the domain to be the collection of things in any world, or else they have an idea of things being present in multiple worlds.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeAug 2nd 2023
    • (edited Aug 2nd 2023)

    I have added (here) a pointer to subtype, for clarification of the notation.

    diff, v15, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeAug 2nd 2023

    There is a curious phenomenon in public discussion of subtleties in physics, which sometimes degenerate with physicist participants insisting to identify as unskilled in math. Here I sense an analog with philosophers identifying as unskilled in formal logic. It’s dubious that giving in to such regressive behaviour is doing any good.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 2nd 2023

    I’m sure they take themselves to be highly skilled in logic. But that’s very much sticking to their favoured logics. Untyped (unityped) logic is the order of the day. It’s not just the commitment to a certain logic, but the associated belief that this commitment comes with a preferred metaphysical point of view.

    You see this when in a slight departure from untyped logic to so-called free logic, which is looking to distinguish entities that ’really’ exist from entities in general, e.g., to include Pegasus the flying horse, it’s not just seen as the obvious extension that it is.

    Essentially, it’s a sorted logic over two sorts, i:D↪Ei: D \hookrightarrow E, where DD are the really existent things. Then we have ’inner’ and ’outer’ quantifiers for the two domains, and their relations, e.g., defining the inner in terms of the outer:

    • ∃xA= defΣx(E!x&A)\exists x A =_{def} \Sigma x(E!x \& A).

    Of course this just follows in DTT from ! E⋅i=! D !_E \cdot i = !_D, and so ∑ E∑ i=∑ D\sum_E \sum_i = \sum_D (or truncations thereof).

    But, no, a great deal of space is devoted to the need for all this, how we need the true ’exists’ for DD and the outer quantifier for EE. Those who haven’t made this move have to deal with the problem that if they agree to ’Pegasus = Pegasus’, then this implies that ∃x(x=x)\exists x (x= x) and they seem to be committed to the existence of Pegasus. But then they can’t deny ’Pegasus = Pegasus’ either.

    So maybe there’s a distinction with physicists only showing interest in the mathematics they know, where the philosophers don’t just stick to the logic they know because they think it’s pragmatically sufficient. They also think it corresponds to how things really (metaphysically) are.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeAug 2nd 2023

    I have now added (here) the existence of the “hexagon of epistemic entailments” which I had mentioned in comment #1.

    I am going on about this hexagon because it turns out to be somewhat interesting at least in the case of linear S5 logic regarded as quantum effect logic (though this is not mentioned yet in the entry).

    diff, v16, current

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 2nd 2023

    Taking the hexagons together, might it be called the “cube of epistemic entailments”?

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 3rd 2023

    I can’t think that these hexagons would have occurred to modal logicians, as they’re saying that for modal propositions, PP and QQ, where PP implies QQ, there are six equivalent derivations of □P\Box P implies ◊Q\lozenge Q. It would only occur to someone interested in proof-relevant modal logic.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeAug 3rd 2023

    Am being distracted today by running errands, but for a preview of what I am after see the diagram here.

1 to 17 of 17

  1.