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.
An elementary question, which may just show my ignorance:
Given a pair of endofunctors , equipped with natural transformations of the form
and
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?
added pointer to what I gather is the origin of the terminology “S5”:
Philosophers frequently now take propositions to be subsets of worlds. So rather than
they would take that itself to be a proposition, i.e., a map from to truth values.
No big difference. We might say that is a -dependent proposition. But it does incline them to see only one fixed locus of variation, rather than treat as itself a variable.
This is classically the same thing: is classically the set of truth values and is a proposition about the elements of .
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.
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)
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.
I was pointing out that many philosophers will be confused with the formulation since for (many of) them, . A proposition is just a predicate on worlds.
They’ll think you’re writing .
The notation is standard and used, for what it’s worth, all over the nLab (starting with Prop).
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.
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.
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, , where 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:
Of course this just follows in DTT from , and so (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 and the outer quantifier for . Those who haven’t made this move have to deal with the problem that if they agree to ’Pegasus = Pegasus’, then this implies that 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.
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).
Taking the hexagons together, might it be called the “cube of epistemic entailments”?
I can’t think that these hexagons would have occurred to modal logicians, as they’re saying that for modal propositions, and , where implies , there are six equivalent derivations of implies . It would only occur to someone interested in proof-relevant modal logic.
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