David Corfield
graded modality

See nLab: graded modality

Case 1

The decomposition of Worlds as a context gives one form of grading. With more subtle dependency graph there would be a directed category of modes. So

H /WH \mathbf{H}_{/W} \stackrel{\longrightarrow}{\stackrel{\longleftarrow}{\longrightarrow}} \mathbf{H}

factoring as

H /WH /W 2H /W 1H \mathbf{H}_{/W} \stackrel{\longrightarrow}{\stackrel{\longleftarrow}{\longrightarrow}} \cdots \stackrel{\longrightarrow}{\stackrel{\longleftarrow}{\longrightarrow}} \mathbf{H}_{/W_2} \stackrel{\longrightarrow}{\stackrel{\longleftarrow}{\longrightarrow}} \mathbf{H}_{/W_1} \stackrel{\longrightarrow}{\stackrel{\longleftarrow}{\longrightarrow}} \mathbf{H}

provides a model for graded modalities, where the grading is via the direct category of the context extension maps.

Case 2

One could make sense of the distinction between Brandom’s:

  1. There is a red apple.
  2. There is an apple which seems to be red.
  3. There seems to be a red apple.

Decreasing amounts are being committed to. ‘Seems to seem’ = ‘seems’, so idempotent. X is P implies X seems to be P.

So two modes for confidence level, or three modes for commitment to coloured fruit, to fruit and to nothing?

Expression of lack of commitment as an effect. The ‘maybe’ monad.

Case 3

Temporal operators as graded, G(t 1)G(t_1) and G(t 2)G(t_2), when t 1<t 2t_1 \lt t_2.

Case 4

Graded by contexts. Different knowledge states of agents. Curry’s construction. Comparing someone relying on AA with someone not, for the latter it’s like the reader monad, P(AP)P \mapsto (A \to P).

Case 5

So can’t we see any Galois connection as a kind of modal (propositional) logic, with two modes?

Case 6

Families of modalities as parameterized HITs

Case 7

Similar to #1, take a type and a collection of equivalence relations. Necessity indexed by R iR_i at a point in the set is of a property holding all over that class.

Case 8

Could have graded reader monads too.

Case 9

Something that continues to puzzle me about analytic philosophy is its devotion to untyped logic. One conceptual tangle that ensues from this choice is what to make of quantifiers such as ‘all’. (On the one hand, we seem to quantify universally over different domains; on the other, our logic contains a single universal quantifier. Now, of course, to achieve quantification restricted to entities with property AA, one may just write x(A(x))\forall x(A(x) \to \ldots).

However, the quantifier variance supporters are not satisfied. The ‘every’ and ‘all’ of our speech to them mean something different depending on what follows. Now, anyone with a background in typed or sorted logics is likely to think of this variance as typed or sorted.

Can it really be as late as 2016 that Hans Halvorson notes

“To date, none of the numerous discussions of quantifier variance have noted the relevance of many-sorted logic.”

https://www.princeton.edu/~hhalvors/papers/collapse.pdf

He then proceeds to resolve the debate in these terms.

Let’s take things up a notch with dependent type theory. Then, yes, there’s a univocality to universal quantification: it arises from the dependent product type formation rule (dependent function, some call it). And, yes, there’s variation in that dependent products are indexed by types, and indeed by functions between types.

A predicate, PP, of type DD is sent to the proposition x:DP(x)\forall x:D P(x).

But given a function f:DEf: D \to E, there’s a predicate on EE, fP(y)\forall_f P(y), which asks at e:Ee:E, is PP the case at all the preimages under ff? fP(e)\forall_f P(e) is true if d:D(f(d)=eP(d))\forall_{d:D}(f(d) = e \to P(d)). nLab

An example of the latter is nation:PersonCountrynation: Person \to Country, where nationHappy(y)\forall_{nation}Happy(y) is the property of a country, yy, that all of its people are happy.

So there we are, quantifier variance aplenty. Now onto graded modalities.

Graded modalities (https://ncatlab.org/nlab/show/graded+modality) date back to philosophical work in the 70s, but the interesting work today is being done by linguists, such as @DanLassiter, and computer scientists, such as my colleague at Kent @dorchard.

One way to achieve a collection of such modalities arises out of the quantifiers we have just seen.

We’ve seen how along a map f:DEf:D \to E, dependence on DD can be mapped to dependence on EE. Then a simple map brings us back in the opposite direction.

Composing these maps gives us an operator from DD-dependent properties to itself. In the person-country case, it sends a predicate of a person, say, happy(x), to another such, all_compatriots_happy(x). (Details in Chap 4 of my book.)

It’s acting like a necessity operator, capturing the situation where a property holds under variation. It’s not just that you’re happy, all of your compatriots are happy too. We can then modify the mapping to give a finer discrimination, e.g., to country region.

A graded set of modalities may be derived from a series of onto mappings f i:DE if_i: D \to E_i, each E iE_i mapping onto the next. For an element of DD, operators are expressing invariance under lesser or greater variation. The operators themselves compose.

Many variants on this theme are possible, but we can already begin to see, e.g., how degrees of obligatoriness, etc., can be captured by the ranges of situations in which an action is required.

The idea of a sequence of epimorphisms seemed apt since epis from a fixed object form a preorder, and so composing two of these modalities results in invariance under the coarser class. We could also consider non-symmetric relations, RR as subobjects of D×DD \times D. Then consider the span of projections DRDD \leftarrow R \to D, and dependent product along p 1p_1, followed by base change along p 2p_2. (A form of ‘intermodality’ https://arxiv.org/abs/2101.10490 .)

Then we’d have modalities graded by all relations, and composition via composition of relations.

Works

Daniel Lassiter, Graded modality, OUP, Lassiter, Graded Modality

Last revised on September 19, 2021 at 13:20:08. See the history of this page for a list of all contributions to it.