Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: what is a modality?

Reid Barton (Oct 06 2020 at 15:02):

Sorry if this is a rude question. Do the words modal/modality mean anything?
It seems that different authors use them in different ways and I haven't been able to determine what (if anything) they have in common.

Dan Doel (Oct 06 2020 at 15:12):

I'm not sure there's any way to subsume all the different ways its used. The closest you might get is, "the interpretation in (pre)sheaf models is not a point-wise construction." :smile:

Dan Doel (Oct 06 2020 at 15:14):

I don't know if that even works, though.

Dan Doel (Oct 06 2020 at 15:20):

I guess another answer is that you have more than one category, and the multiple categories are related in some way reflected in the logic/type theory. But that is not always obvious.

Henry Story (Oct 06 2020 at 17:43):

I think intuitively Modal Logic comes up when quantifying over contexts.
Compare traditional logic and old fashioned possible world semantics. In the second case you quantify over all the different ways things can be, which you can think as idealized models (databases which record every fact in a universe). In traditional logic you work with a model, but don't speak of the models themselves. (Unless you extend ontology to include models as David Lewis shows how to do in Counterfactuals if I remember correctly ).

This web site that builds on a PhD thesis Coeffects: Context Aware Programming which made me think this is a fruitful way to think of this.

Jens Hemelaer (Oct 07 2020 at 13:57):

One of the common themes seems to be that there are additional unary operators, for example the square or the rhombus on the Wikipedia page. At the topos level, such an additional unary operator is apparently often a monad.

For example, you can look at a presheaf topos $\mathbf{PSh}(\mathcal{C})$ together with the sheafification monad associated to some Grothendieck topology $J$. Then in the corresponding modal logic, you can express that a statement holds in the presheaf topos, but you can also express that the statement holds in the sheaf subtopos $\mathbf{Sh}(\mathcal{C},J)$, using the unary operator. The operator then means "this proposition might not be valid but it is valid locally".

You can find this example and other on the nlab here.

Reid Barton (Oct 07 2020 at 14:49):

Jens Hemelaer said:

such an additional unary operator is apparently often a monad

I guess this gets to the point of my question. There seem to be at least two ways to use the word "modality". One is with a specific definition, as here and here. But I don't understand why the authors chose that specific word, or that specific definition; and at any rate as they explain they don't try to include all modalities under their definition.
The other way seems to be an example of a https://ncatlab.org/nlab/show/concept+with+an+attitude: "something you might denote by a square or a diamond". But I don't understand what the concept is supposed to be...

Reid Barton (Oct 07 2020 at 14:54):

So, in the end, I'm not sure what things are appropriately described as "modalities", and which things not. But I imagine that something like $\Box P = \lnot P$ would generally not be considered a modality.

Spencer Breiner (Oct 07 2020 at 14:56):

I wouldn't usually think of negation as a modality, because it is contravariant, but double negation is.

Henry Story (Oct 07 2020 at 15:40):

Jens Hemelaer said:

One of the common themes seems to be that there are additional unary operators,

You can also have binary operators such as Lewis counterfactual modalities: $\text{Kangaroos have no tails} \mathrel{\mathop\Box}\mathrel{\mkern-2.5mu}\rightarrow \text{Kangaroos topple over.}$
meaning "in the closest worlds in which Kangaroos have no tails, they topple over" or "If kanagroos had no tails they would topple over". I posted a few pictures on that on twitter recently. There seems to be a topological dimension there. So I really need to read @Tai-Danae Bradley's book (so much to do).

@valeriadepaiva @emilyriehl That's C.I.Lewis's 1932 S4 modal logics. David Lewis in 1973 does build Counterfactuals on nested spheres of worlds equipped with a similarity relation. So "If Kangaroos had no tails they would topple over" => in the closest worlds in which kangaroos have tails they topple over. https://twitter.com/bblfish/status/1308236842836385792/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

John Baez (Oct 07 2020 at 15:43):

But I don't understand what the concept is supposed to be...

I'm not sure what level of non understanding you're talking about here. So let me start with the obvious stuff you probably do understand. A modality is, classically, a way of saying that a proposition is true in some way. The famous ones are

P is possibly true.
P is necessarily true.
P should be true.
P will sometime be true.
P will always be true.
P was sometimes true.
P was always true.

One can check that these tends to be monads (aka "closure operators") or comonads (aka "interior operators"). E.g.

If it was always true that P was always true, then P was always true.

If P is possibly true then P is possibly possibly true.

Dan Doel (Oct 07 2020 at 15:45):

@Reid Barton The second characterization I gave is arguably more general, and might be fleshed out like this: you want to incorporate reasoning about multiple interrelated judgments in a single system. Each judgment form is a 'mode', and may have somewhat different rules for how the reasoning works in that mode.

In normal logic, there is only one reasoning mode, about 'truth'. Then every modal logic adds some choices of other reasoning modes. Maybe we also reason about provability/derivability, or 'is always true' vs. 'is true right now' (the latter being what 'truth' is repurposed as). One step toward this is to have multiple judgment forms like $Δ; Γ ⊢ A\ \mathsf{true}$ vs. $Δ ⊢ A\ \mathsf{deriv}$, and have rules for deriving both sorts of judgments. This roughly corresponds to having as many categories (for the semantics) as there are modes.

However, it might also be desirable to be able to reflect one sort of judgment in terms of another, and this is what modalities do. So, there is a correspondence between, say, $A$ being judged derivable and $\square A$ being judged true. Sometimes this can allow you to make some of the modes redundant. For instance, 'derivability' has essentially the same structure as 'truth', except there are no 'local' premises. So you could get rid of reasoning in 'derivability' mode and just have a rule where $Δ; ⊢ A\ \mathsf{true}$ lets you deduce truth of $\square A$, and some rules about how $\square$ distributes over connectives and such. Then all reasoning in one mode can be replaced by reasoning in another mode, by using statements involving modalities.

Reid Barton (Oct 07 2020 at 15:50):

Well, as a contrasting example, I do understand what, say, a monad is: it's a functor $T : C \to C$ equipped with some more structure such that blah blah blah. I don't have to understand the concept of what it means to be a monad through a list of examples, or through a list of ways in which monads get used, because there is an actual definition.

Henry Story (Oct 07 2020 at 16:04):

@Reid Barton I think there is an ongoing process of discovering what Modalities are. Clearly humans have used temporal, counterfactual, local, deontic and other modalities since the dawn of civilization. Understanding what they are mathematically is a process of discovery.

It may be that the Modal HoTT people are getting to give a full overview of how best to understand all of them together.
There is also the older and very clear work by @Corina Cirstea and @Alexander Kurz Dirk Pattinson and @Lutz Schröder Modal Logics are Coalgebraic. (And I wonder how that view ties in with the up-and-coming HoTT one.) But the idea there is that coalgebras are the mathematics of processes. Which way a process goes depends on a decision (someone pushing a button on a coffee machine), which changes the state of the process. In coalgebras one is always in a state. The modalities arise if one wants to assert properties of all future (or past) states, some states, the next ones, etc....

Reid Barton (Oct 07 2020 at 16:10):

So it seems to me that in this broad sense, "modality" has no object-level meaning. For example, it doesn't make sense to write "Proposition. Let $\Box$ be a modality. Then ..."

John Baez (Oct 07 2020 at 16:12):

Reid Barton said:

Well, as a contrasting example, I do understand what, say, a monad is: it's a functor $T : C \to C$ equipped with some more structure such that blah blah blah. I don't have to understand the concept of what it means to be a monad through a list of examples, or through a list of ways in which monads get used, because there is an actual definition.

Oh, okay, so by "understand" you meant "know the definition of". I would say modality isn't like that: it's something people are trying to formalize in different ways, where you can only make progress on formalizing it if you have some intuitive feel for it that you get through examples.

Of course you can accept someone else's formalization: I feel sure people have written definitions of "modality" - if they haven't I could write one right now! - but then you're trusting that they're on the right track.

Reid Barton (Oct 07 2020 at 16:16):

But I guess I don't really understand why the situation is this way. Suppose I write down a series of operators $\Box : \mathrm{Type} \to \mathrm{Type}$ starting with $\Box P = \lnot P$ (least likely to be a modality) and ending with $\Box P = P$ (most likely to be a modality, I guess!) Will everyone agree about which elements on the list are modalities and which aren't? If so, doesn't that suggest that there is some objective criterion being applied? If not, what does it imply for the concept of "modality"?

Reid Barton (Oct 07 2020 at 16:17):

John Baez said:

I once met a mathematician who asked me to define an "electron"....

I actually also thought that it feels less like a concept of mathematics and more like a concept of physics or computer science.

John Baez (Oct 07 2020 at 16:17):

I deleted the comment you just responded to because I decided it was too obnoxious.

John Baez (Oct 07 2020 at 16:18):

But anyway, I think of this as a good intro to modal logic:

https://plato.stanford.edu/entries/logic-modal/

John Baez (Oct 07 2020 at 16:18):

and you'll see people are still, after about 2500 years, grappling with trying to understand "modalities".

Reid Barton (Oct 07 2020 at 16:23):

Well, I didn't mind and I already apologized for the obnoxiousness of this whole discussion in my first message.

Dan Doel (Oct 07 2020 at 16:25):

I think one of the main motivations for modal logic is to internalize something that would otherwise be meta-reasoning. So expecting them to be characterized in terms of what you already have is too limiting, generally.

Reid Barton (Oct 07 2020 at 16:25):

I guess I should emphasize that this question was triggered largely due to the terminology in the arXiv papers I linked above, using "modality" for a specific concept (namely a specific kind of idempotent monad). It made me think that there might be an answer to this question after all.

Reid Barton (Oct 07 2020 at 16:26):

I'm certainly fine with the idea that even in math, there are some words we use that aren't pinned down to specific meanings outside of specific contexts ("homotopy" comes to mind as a possible example).

Dan Doel (Oct 07 2020 at 16:29):

I think $¬$ could be a modality in my explanation. The modes would be reasoning about 'truth' and 'falsity'. $¬$ lets you reason about falsity in terms of truth.

Dan Doel (Oct 07 2020 at 16:30):

That is too old, though, and grandfathered into not being considered a modality.

Dan Doel (Oct 07 2020 at 16:34):

It even fits my other definition in intuitionistic logic, because the semantics are not point-wise.

Nathanael Arkor (Oct 07 2020 at 16:37):

The viability of considering negation as a modality is discussed on the Stanford Encyclopedia of Philosophy (Negation).

Dan Doel (Oct 07 2020 at 16:39):

For a lot of definitions you can come up with, implication qualifies as a modality.

Dan Doel (Oct 07 2020 at 16:40):

For instance, its rules aren't uniformly parameterized by a context, if you use contexts.

Dan Doel (Oct 07 2020 at 16:43):

And the natural deduction rule for implication in older systems that don't use contexts has a sort of partial deduction as a premise (like '$A\ \mathsf{true} ... B\ \mathsf{true}$'), which seems like "internalizing meta-reasoning".

Dan Doel (Oct 07 2020 at 16:44):

If you can meta-reason that $B$ is deducible from $A$, then you can conclude $A → B$.

Dan Doel (Oct 07 2020 at 16:47):

Oh, also, it's coalgebraic, usually.

Reid Barton (Oct 07 2020 at 16:57):

Dan Doel said:

I think one of the main motivations for modal logic is to internalize something that would otherwise be meta-reasoning. So expecting them to be characterized in terms of what you already have is too limiting, generally.

In this context I'm just interested in what the external concept that we're trying to internalize was in the first place, i.e., what are the intended semantics corresponding to things we call modalities. For example, I'm pretty sure left-exact localizations qualify under any definition of modality.

sarahzrf (Oct 07 2020 at 16:59):

i would take a bit of a pl/logic attitude toward modalities personally

sarahzrf (Oct 07 2020 at 17:00):

i would say that a modality is a marker for a shift in semantics, sort of

sarahzrf (Oct 07 2020 at 17:01):

like, you write □P to say that, instead of interpreting P like you were ordinarily about to, you perform some shift in your understanding of what process you're following to extract semantic content from P

Dan Doel (Oct 07 2020 at 17:03):

@Reid Barton I'm not sure any definition is general enough other than 'a monad or a comonad', then. And even that might be wrong.

sarahzrf (Oct 07 2020 at 17:03):

like for example...

sarahzrf (Oct 07 2020 at 17:04):

we have alethic modalities, epistemic modalities, etc—and those fit what i just said insofar as like

sarahzrf (Oct 07 2020 at 17:06):

handwavily: let's say, at any given point in a claim i make, i have an existing implicit understanding of under what contingencies, or in what sense, etc etc, i am asserting P

sarahzrf (Oct 07 2020 at 17:07):

if i say "necessarily P", then rather than asserting P in the existing context, i am indicating a context shift—the claim P nested inside the modality is to be understood as differently contextualized/qualified; it holds more generally than under the contingencies i was taking for granted

Dan Doel (Oct 07 2020 at 17:07):

I mean, it is wrong for the false/not example. So in that case you need to weaken it to some kind of embedding between two categories.

sarahzrf (Oct 07 2020 at 17:07):

if i say "that guy believes P", then rather than asserting P in the existing context, i am shifting to the context of "the beliefs held by that guy" before making my assertion

sarahzrf (Oct 07 2020 at 17:08):

if i say "later P", in the step-indexing sense, i am shifting my timescale before making an assertion

sarahzrf (Oct 07 2020 at 17:10):

and then kripke semantics tends to do well by modal logic because "possible worlds" captures quite a few of the useful examples of this "switching to a new semantics"—often, the new mode of interpretation intended is just the old one with an altered value of some parameter

sarahzrf (Oct 07 2020 at 17:10):

and even if it isn't naturally, you can often force it into that mold

sarahzrf (Oct 07 2020 at 17:14):

anyway my Take is that modalities are commonly monads because ummm

Henry Story (Oct 07 2020 at 17:15):

that's an interesting question. What do modalities have to do with adjunctions. :-) (obviously there are two contexts in the form of two categories).

sarahzrf (Oct 07 2020 at 17:18):

uncooked thoughts alert:
it's something like: you have a number of different categories and semantics in each of them, and these are all possible modes of interpretation of your language—and a modality expresses a shift from one mode of interpretation to another, so, uh, something something compositionality something something functor, and then in the event that there's an adjunction, this manifests as monads and comonads

John Baez (Oct 07 2020 at 17:23):

It's possible ordinary folks don't have the mental resources to really think about "possibly possible" meaning anything other than "possible". Philosophers talk about possible world semantics, where "possibly P" means "in some world P". But then they argue about whether "possible" means the same thing in every world! Maybe "possibly P" means "in some world close enough to mine that I can imagine it, P". But then maybe someone in a world close enough to yours that you can imagine it can imagine a world you can't imagine! Yes, philosophers have actually discussed this.

John Baez (Oct 07 2020 at 17:25):

In this world, ordinary people just don't say "possibly possibly P", so there's no standard meaning.

John Baez (Oct 07 2020 at 17:28):

Well, I guess people sometimes say "it could be possible..."

John Baez (Oct 07 2020 at 17:29):

But anyway, this lack of a strong standard practice means mathematicians are somewhat free to make up new rules when they formalize this modality, following dictates like "elegance" and "logical coherence". E.g.: "I want it to be a comonad!"

sarahzrf (Oct 07 2020 at 17:32):

i think step indexing's "later" is a good example of a unary connective which is

1. clearly a modality
2. neither a monad nor a comonad (doesn't even admit a transformation from its square)

Henry Story (Oct 07 2020 at 17:48):

Interesting. That's the step-indexing from this cs-theory question I guess.

Dan Doel (Oct 07 2020 at 17:53):

It probably generalizes to some kind of graded monad, right?

Dan Doel (Oct 07 2020 at 17:54):

Although the generalization might also be a graded comonad.

Dan Doel (Oct 07 2020 at 18:02):

$\rhd$ is one step later, $\rhd_n$ is $n$ steps later. $\rhd_m\rhd_n \simeq \rhd_{m+n}$ etc.

sarahzrf (Oct 07 2020 at 18:15):

ya henry

sarahzrf (Oct 07 2020 at 18:25):

the extremely glib summary that explains nothing whatsoever but which i can type quickly is:

• take PSh(N) (where N is the poset of natural numbers with the usual ordering)
• the successor function S : N → N is monotone, so that's an endofunctor on N. flip it and get S^op : N^op → N^op; now Ran_{S^op} : PSh(N) → PSh(N) exists since N^op is small and Set is complete. call this endofunctor "later".
• that's a right adjoint, so it preserves subterminal objects, i.e. truth values in the topos. hence, it restricts to a modality on truth values in particular.
• more generally, there's an endomorphism of Ω which is related somehow to the endofunctor by some sort of pullback which i don't care to remember. there's some fibered fnuctor stuff going on

sarahzrf (Oct 07 2020 at 18:31):

anyway, a truth value in PSh(N) is a downward-closed subset of N, and the action of this functor on such a thing is to "extrude it upward by a step"—empty set goes to {0} and {0} goes to {0, 1} and so on, N goes to itself

Reid Barton (Oct 07 2020 at 18:49):

Is this a fair summary?

• In logic/type theory, a "modality" is "an operation on propositions/types that one might denote by the symbol $\Box$ or $\Diamond$", following the tradition of modal logic, and its semantics will be whatever is appropriate to the situation, usually (but maybe not always) a (co)monad.
• In HoTT (specifically section 7.7 of the HoTT book), a "modality" means an operation on types satisfying specific properties, but these specific properties don't really have anything to do with the situations in which we would use the word "modality" in general.

Dan Doel (Oct 07 2020 at 18:52):

I don't think the HoTT modalities have nothing to do with the former thing.

Reid Barton (Oct 07 2020 at 18:53):

Well people here don't even seem to want to commit to the idea that a modality should be a functor, let alone that it satisfies the equivalent conditions of Theorem 7.7.4 or whatever.

Reid Barton (Oct 07 2020 at 18:53):

So, it seems to me largely arbitrary to choose this specific word for this specific concept. No?

Dan Doel (Oct 07 2020 at 18:54):

Right. It's too restrictive. But they're probably all modalities in the former sense.

Dan Doel (Oct 07 2020 at 18:55):

I think it was lifted from a category theoretic characterization of a particularly well behaved class of the former modalities.

Dan Doel (Oct 07 2020 at 18:55):

Where the modality arises from a (co)reflective subcategory.

Nathanael Arkor (Oct 07 2020 at 18:58):

So just idempotent (co)monads?

Dan Doel (Oct 07 2020 at 18:58):

Yeah.

Reid Barton (Oct 07 2020 at 18:58):

The definition in the HoTT book is more specific than just an idempotent monad though--there's also these conditions of Thm 7.7.4

Reid Barton (Oct 07 2020 at 18:59):

And for some reason, it's specifically under these extra conditions that they use the term "modality".

Reid Barton (Oct 07 2020 at 19:02):

I don't really understand these conditions on an intuitive level. And I also don't understand the usage of the term "modality" in the broader sense (let's say for something which is already an idempotent monad). But my sense is that understanding one of these will not help with the other.

Reid Barton (Oct 07 2020 at 19:04):

My sense is they needed a word for this condition and the word "modality" was available.

Henry Story (Oct 07 2020 at 19:06):

Well they do say:

(More precisely, we should perhaps call these idempotent, monadic modalities

Some of the authors then went on to work on Modal HoTT, so I think they were aware of the limitations of working within HoTT. (see discussion above on Modal HoTT (and here). Modal HoTT extends to geometric morphism between $(\infty , 1)$-topoi.

Dan Doel (Oct 07 2020 at 19:12):

It seems like they just want to ensure it's perserving the 'small' type formations, so that it's like a "reflective sub-type-theory," but one isn't automatically implied by their initial characterization of a reflective subuniverse.

Dan Doel (Oct 07 2020 at 19:12):

I.E. some people would say that their definition of a "reflective subuniverse" is actually not a universe, because it's not closed under Σ types.

Henry Story (Oct 07 2020 at 19:19):

It may be a bit confusing in that Modal HoTT may be thought to the Modal chapter in the HoTT book, whereas really it refers to a project to extend HoTT to geometric morphisms between HoTT spaces.

Reid Barton (Oct 07 2020 at 19:29):

Right! I only learned this recently myself and I haven't had a chance to look at the Modal HoTT book yet. I think the title is a bit unfortunate from a mathematician's perspective. If you care about the internal logic of a ($\infty$-)topos then, considering how important the relative point of view is in algebraic geometry, surely you also care about the internal logic of two topoi related by a geometric morphism.

Jason Erbele (Oct 08 2020 at 15:45):

John Baez said:

Reid Barton said:

Well, as a contrasting example, I do understand what, say, a monad is: it's a functor $T : C \to C$ equipped with some more structure such that blah blah blah. I don't have to understand the concept of what it means to be a monad through a list of examples, or through a list of ways in which monads get used, because there is an actual definition.

Oh, okay, so by "understand" you meant "know the definition of". I would say modality isn't like that: it's something people are trying to formalize in different ways, where you can only make progress on formalizing it if you have some intuitive feel for it that you get through examples.

Of course you can accept someone else's formalization: I feel sure people have written definitions of "modality" - if they haven't I could write one right now! - but then you're trusting that they're on the right track.

In a way, this reminds me of the status of the word "planet" in astronomy, prior to 2006, when the International Astronomical Union finally agreed on a definition for that term. Planets have been discussed for thousands of years, and science fiction explored the idea of extrasolar planets that most people would agree are planets, in the context of the story. Some definitions proposed were deemed too strict (e.g. "has a moon" would exclude Mercury and Venus). The 2006 IAU definition didn't really satisfy everyone, either – Pluto had been considered a planet for about 75 years, and now it suddenly isn't. I wonder if the current state of the word "modality" is the same state of limbo that "planet" was in 15 years ago.

Jules Hedges (Oct 08 2020 at 16:05):

I wonder what the history of the modality concept is... I'd guess it's "really" a term of linguistics (modal verbs) that got stolen by analytic philosophy, and from there made its way into mathematical logic

Jules Hedges (Oct 08 2020 at 16:08):

That is, I'd guess people were classifying how words like "should" and "must" behave grammatically in different languages, before anyone had the idea of trying to make operators like "must" in a formal logic

Fawzi Hreiki (Oct 08 2020 at 16:12):

The notion of a modality surely existed before analytic philosophy (if by analytic philosophy you mean post-Frege British and American philosophy)

Fawzi Hreiki (Oct 08 2020 at 16:13):

https://plato.stanford.edu/entries/leibniz-modal/

Fawzi Hreiki (Oct 08 2020 at 16:15):

I would even say that Leibniz thought about modality in a quite mathematical way (albeit not as we do now)

Fawzi Hreiki (Oct 08 2020 at 16:27):

Also, to add on to that, I think that trying to find a precise mathematical definition of 'modality' is like trying to find a precise definition of 'space' or 'number'. It is neither tenable, nor even desirable as any definition will either be too general or too restrictive (probably even both) rendering it useless.

John Baez (Oct 08 2020 at 16:41):

Modal logic is very old... this Wikipedia mini-history is nice:

The basic ideas of modal logic date back to antiquity. Aristotle developed a modal syllogistic in Book I of his Prior Analytics (chs 8–22), which Theophrastus attempted to improve. There are also passages in Aristotle's work, such as the famous sea-battle argument in De Interpretatione §9, that are now seen as anticipations of the connection of modal logic with potentiality and time. In the Hellenistic period, the logicians Diodorus Cronus, Philo the Dialectician and the Stoic Chrysippus each developed a modal system that accounted for the interdefinability of possibility and necessity, accepted axiom T (see below), and combined elements of modal logic and temporal logic in attempts to solve the notorious Master Argument. The earliest formal system of modal logic was developed by Avicenna, who ultimately developed a theory of "temporally modal" syllogistic. Modal logic as a self-aware subject owes much to the writings of the Scholastics, in particular William of Ockham and John Duns Scotus, who reasoned informally in a modal manner, mainly to analyze statements about essence and accident.

C. I. Lewis founded modern modal logic in a series of scholarly articles beginning in 1912 with "Implication and the Algebra of Logic". Lewis was led to invent modal logic, and specifically strict implication, on the grounds that classical logic grants paradoxes of material implication such as the principle that a falsehood implies any proposition. This work culminated in his 1932 book Symbolic Logic (with C. H. Langford), which introduced the five systems S1 through S5.

Dan Doel (Oct 08 2020 at 16:42):

Well, it might not be useless. Just not useful for everyone.

I suppose this line of thought reminds me of a pet peeve of mine. An example is where people jump into a conversation and say, "actually, tomatoes are a fruit." But that is a technical classification by botanists (I think), who borrowed the word "fruit" from common language and gave it a technical definition that suits their purposes. But there's no reason to presume that botanists chose the best precise definition for anyone but themselves, and that we all need to bow to their decision.

I think "berry" is an even worse example (and there are a lot of others).

Henry Story (Oct 08 2020 at 17:08):

Mathematical/logical/formal based thought about Modalities has been very useful in many areas.
In philosophy the mathematical structures put forward by Kripke and Hintikka overturned conceptions of what was a legitimate argument. Bertrand Russel, could not find a space for modal logic, and so, having provided a foundation of all of logic and mathematics on set theory, deemed certain types of thinking irrational and "magical". The introduction of precise formal proofs of modal logic completely overturned the analytic school started by Russel, since their dedication to mathematical precision had led them to a point where they could see the logic behind what Russel would have considered just metaphysics (a very bad word at the time).

More practically, modal logics are it seems growing in importance in computing with languages such as Rust adopting linear logic for reference counting, granule extending it with graded modalities, ... I think as one studies these, one starts seeing the relation between all these areas, and why they are called modalities.
It is very much like the word "number": initially it was natural numbers (without 0) then N then Z then R then imaginary numbers, and I am sure more :-)

The space of graded modalities spans many fields: from programming languages such as #Granule all the way to a whole field of modal logics from Counterfactuals, to epistemic and deontic logics, ... See a survey from this year by @DanLassiter https://web.stanford.edu/~danlass/Lassiter-book-draft.pdf https://twitter.com/bblfish/status/1195393138661216256

- The 🐟‍‍ BabelFish (@bblfish)

Dan Doel (Oct 08 2020 at 18:10):

There is also "contextual modal logic/type theory", which has modalities that look like $\left [x:A,y:B,z:C \right ] D$. Though you could conceivably present it in a way that makes the modality look more standard (by making the thing it applies to fancier).

sarahzrf (Oct 08 2020 at 18:42):

contextual modal type theory :heart:

sarahzrf (Oct 08 2020 at 18:43):

i played around with beluga a bit and i swear it was like a vision of the future

sarahzrf (Oct 08 2020 at 18:43):

okay maybe i care more about binding and scope than most people

Dan Doel (Oct 08 2020 at 18:43):

Yes, it's quite interesting.

Dan Doel (Oct 08 2020 at 18:44):

I actually like their notation a lot more (because I also came up with it myself, I think): $\left [ x:A, y:B, z:C ⊢ D \right]$

sarahzrf (Oct 08 2020 at 18:44):

i really need to read up on whatever andrew pitts has been up to >_<

sarahzrf (Oct 08 2020 at 18:47):

i googled to see if anyone had phrased/done stuff w/ day convolution in the schanuel topos yet and i hit the jackpot and ive been putting off doing the actual reading for a while now :pensive:

sarahzrf (Oct 08 2020 at 18:47):

image.png

sarahzrf (Oct 08 2020 at 18:52):

i absolutely love the concept of the И quantifier & i want to see a billion more variations on that theme

Dan Doel (Oct 08 2020 at 18:52):

Oh, well, I have something for you to look at, then.

Dan Doel (Oct 08 2020 at 18:53):

https://arxiv.org/abs/2008.08533

Dan Doel (Oct 08 2020 at 18:54):

That attempts to show how to integrate a bunch of extensions to type theory incorporating presheaf features, including nominal stuff, but also cubical, and all sorts of other examples.

sarahzrf (Oct 08 2020 at 18:55):

into the zotero it goes

sarahzrf (Oct 08 2020 at 18:55):

maybe someday i'll remember it exists

sarahzrf (Oct 08 2020 at 18:55):

:sob:

Dan Doel (Oct 08 2020 at 18:57):

Maybe integrate is the wrong word. It's trying to show how they're all instances of the same sort of construction.

sarahzrf (Oct 08 2020 at 18:57):

neat

Dan Doel (Oct 08 2020 at 19:00):

I kind of hope someone gives it a better name, though.

sarahzrf (Oct 08 2020 at 19:04):

btw before i forget the topic, just wanted to finish saying:

• it feels an awful lot to me like separation logic and nominal logic / nominal techniques are both manifestations of an underlying phenomenon of "genericity" and/or "generativity" and/or "non-interference"
• in both cases, monoidalness and/or substructurality seems to be critical, or at least relevant, and i guess in part in order to ensure that the freedom to make genericity assumptions doesn't get violated
• i really want there to be a way to import the common phenomenon from pl to, say, geometry, to do stuff like give a framework for "generic position" arguments or sth

Dan Doel (Oct 08 2020 at 19:11):

I think that is part of that paper. The 'transpension' operation seems like a way of making up a 'generic' value to feed into a value with a Π type. From what I gather, this is kind of degenerate in the nominal case, because Σ = Π. But it is novel in the other contexts.

Dan Doel (Oct 08 2020 at 19:20):

One thing to keep in mind for concrete examples is that the Σ and Π they're talking about don't always show up as normal types. In cubical type theory Π is PathP, I believe. And Σ is a sort of cylinder.

sarahzrf (Oct 08 2020 at 19:24):

for the record, i actually don't think that last bullet i wrote is even too much of a reach? compare:

• it's fairly established that nominal techniques are naturally understood as dealing with the schanuel topos, so you have sheaves right there, and the fact that there's always new fresh names available comes from the fact that interpreting the internal language sort of introduces implicit passage to covering sieves as necessary, where there are more names
• you have important general position results that say things like "by measure, almost all configurations are in general position" (im probably abusing terminology i dont know what im talking about here lol), and "almost all" is passing to a covering sieve

image.png

sarahzrf (Oct 08 2020 at 19:26):

well, i guess the connection there isn't so much in how they both talk about genericity as in how you can use sheaves to manage both notions... hrm

sarahzrf (Oct 08 2020 at 19:26):

alright this is getting off topic :sweat_smile:

Henry Story (Oct 08 2020 at 19:49):

sarahzrf said:

contextual modal type theory :heart:

:-) I have been researching Modalities in order to understand contexts in RDF. In Context Mereology (2007) Pat Hayes makes the link from RDF to modalities. From FP programming I came to be interested in how that fits in CT, so as to help bridge these two areas. But most of the work relating RDF and CT does not look at Contexts (Eg . Braatz's thesis). The 2010 paper Context Representation for the Semantic Web that looks at it from an Institution Theory perspective, is an exception. But IT has it's limitations as we have heard here.

Henry Story (Oct 09 2020 at 07:59):

I found this 2008 paper Contextual Modal Type Theory. In the "Related Work" section I see the literature crosses with the literature Pat Hayes refers to. (the ist operator ("is true in context")).

Morgan Rogers (he/him) (Oct 09 2020 at 08:58):

Definitely off topic, but oh well: @sarahzrf I had a dive into Jackson's thesis recently, and there is a lot of nice stuff in there, but he gets so close to something much more powerful that I really think it should be fixed. In order to define the sheaf of measures, he starts with the object of "semireals" in a presheaf topos, which is very promising, and then he takes some contrived subobject of this and shows it's a sheaf. I have a strong suspicion that what he ends up with should amount to something akin to the sheaf of semireals in the sheaf topos, but he doesn't explore that idea. If I'm right, then that provides a new analytic way to do measure theory by converting statements therein into statements about semireals, which seem to be much simpler to describe (internally).

sarahzrf (Oct 09 2020 at 14:50):

that sounds fascinating and im sure i would love to discuss it if i had actually read the thesis

sarahzrf (Oct 09 2020 at 14:50):

:sweat_smile:

sarahzrf (Oct 09 2020 at 14:59):

ahh it's the upward-closed subsets of Q

sarahzrf (Oct 09 2020 at 14:59):

(0, 1)-copresheaves

Henry Story (Dec 04 2020 at 09:44):

Dan Doel said:

There is also "contextual modal logic/type theory", which has modalities that look like $\left [x:A,y:B,z:C \right ] D$. Though you could conceivably present it in a way that makes the modality look more standard (by making the thing it applies to fancier).

I got a bit of time to read about Contextual Modal Type Theory and found the recent presentation by Brigitte Pientka: Mechanizing Meta-Theory in Beluga which shows how the theory is used in the Beluga proof assistant and where they are going.. (This is part of Andreij Bauer's proof assistant series).

Henry Story (Dec 04 2020 at 11:45):

The 2008 article on which Beluga is based Contextual Modal Type Theory has a lengthy "Related Works" section which mentions Propositional Logics of Contexts from 1995 (using the is-true-in-context or its operator). It could have mentioned Guha in his 1991 thesis Contexts: a formalization and some applications derived from his work on Cyc. Guha now a Google fellow, then went on to work on the first RDF specs. The logic of contexts was then developed in various papers, but in particular interest to CT, with Institution Theory in Context Representation for the Semantic Web 2010.

Henry Story (Dec 04 2020 at 18:25):

I just discovered this very interesting article from 2020 Knowledge and Simplicial Complexes which models Epistemic Modal Logic in multi agent systems using simplicial complexes.