David Corfield modality

Modality

What if we copied the treatment of modality from the slice of worlds, $W$, to the slice over a proposition, $A$.

Then, we have an arena where $A$ holds, and one where it is not yet established. Pulling back $B$ from the latter, we have $B \wedge A$. For a proposition in the slice, $C \to A$, there is left adjoint, $C$, and right adjoint to $A \to C$.

From the point of view of $H$, the (co)monad is $B \mapsto B \wedge A$, and $B \mapsto A \to B$, both idempotent. So more like reader, writer. $Hom_{H/A}(B \wedge A,C) \equiv Hom_H (B, A \to C)$ and $Hom_{H/A}(C, B \wedge A) \equiv Hom_H (C, B)$.

For $A$ a type and $B$ a property of that type, how do we mark the difference between the following?:

• This A is B.
• This A is necessarily B (by virtue of being A).

For example,

• This coin in my pocket is silver.
• This emerald is necessarily green.

(These are famous examples from Nelson Goodman’s 1955 book Fact, Fiction, and Forecast.)

With propositions as types, it might be that the difference is marked by the form of the element witnessing the truth of the proposition. Where I might look at a gem I know to be an emerald, $e$, and observe that it is green, this would only warrant

• This emerald is green. $\vdash p: Green(e)$

If, on the other hand, I have a witness to a universal statement

• $f: \prod_{x: Emerald}Green(x)$,

then I can apply this function to my gem, $e$, to construct $f(e): Green(e)$.

We can see why the language of necessity is invoked from our analysis of modality here.

When there is variation over a type, $A$, then the necessity operator is applied to a dependent type $x: A \vdash B(x): Type$, as $x: A \vdash \Box_A B(x) := A*\prod_{x:A}B(x)$.

Evaluated at $a: A$, this yields the (non-dependent) proposition $\Box_A B(a) = \prod_{x:A}B(x)$. In other words, the $f$ above is also an element of the necessity of $e$‘s greenness.

However, it can’t just be a question of a true universal statement playing this role. E.g., we might have

• All the coins in my pocket are silver.

In a sense, if all the coins in my pocket are silver, then a choice of such a coin must result in a silver one. On the other hand, there’s evidently a difference since there seems to be no modal element in this case in the following sense. I’ve only taken a look at some of the coins that will ever be in my pocket, those which happen to be there now. Tomorrow there may be copper coins. I could place such a coin there now, whereas I cannot possibly discover a non-green emerald. The issue of a ‘natural’ range of variation arises. A range time-limited to the moment seems unnatural. Then again, I might seal up my pockets never to carry any more. The coins in my pocket now are the only ones which will ever be coins in my pocket, and they all happen to be silver.

But this emerald is necessarily green due to the structural properties it shares will all emeralds. There’s a difference between deriving that the chromium (or possibly vanadium if you’re from North America) infused beryl ($Be_3 Al_2(SiO_3)_6$) composition will entail greenness, and checking that specific gems are green. [NB: we ignore that colour is used in counting such gems as emeralds.]

Goodman set inductive logicians the challenge of making sense of the difference, and seeing that as logical empiricists, and so nervous of modal talk, they hoped to rely merely on syntactical features, it seemed that he had set them a very challenging task.

I once argued that we see just these considerations in the mathematical case in distinguishing lawlike regularities from happenstantial ones, even though all truths of mathematics are taken as necessary in some sense, (Mathematical Kinds).

• All primes of the form $4n+1$ are sums of two squares.

So we see the difference between

• $S(13)$: $13$ is the sum of two squares.

demonstrated via $2^2 + 3^2: S(13)$ versus $p:(13 = 4 \cdot 3 + 1) \wedge Prime(13) \vdash f(13, p): S(13)$, where $f(n, p)$ is something like a constructive proof of the general result from the dependent sum of natural numbers which are prime and of the form $4n+1$.

For a finite type, is there a difference between a law and a list? Can there be a law for one instance?

• All numbers, $n$, equal to $3!$ are such that $S_n$, the symmetric group on that many elements, $\Sigma_n$, possesses an outer automorphism.

The Goldbach conjecture has as instance 18 = 7 + 11. What if we derive a proof of the conjecture as a combination of a general proof for $n$ at least as great as some large number, and a computer check for those below. Are we inclined then to say that 18 is necessarily a sum of two primes in the same way as 13 is necessarily the sum of two squares?

What happens as modality meets dependent types?

Try dependent propositions

• X is happy and they know it.

People may not be happy, or be happy and not know it, or be happy and know it.

• It is possible that (X is happy and they know it).

• X is happy and it is possible that they know it.

• modal type theory

Graded modality

Generalise the slice treatment by having a series of equivalence relations.

If we had a series of types of variation, through multiple epis from one type to others, $F_i: A \to B_1 \to B_2 \to B_3 \to \ldots \B_n$ Then we could have $\Box_i$. Then $\Box_i \Box_j = \Box_{max\{i, j\}}$, and likewise for $\bigcirc_i$.

This represents variation over successively coarser equivalence relations.

Could also have a lattice of epis. Maybe lax then.

Can’t we see Kant’s categorical imperative in his Groundwork of the Metaphysics of Morals as reliance on absolutes? It is absolutely obligatory under all circumstances. Seems that we may well have incompatible duties. Most objections are to taking any imperative as categorical, e.g., ‘It is obligatory under any circumstance to tell the truth’. What if truth-telling brings about harms to one’s moral projects? Note that there are relative duties.

Need to rank order our goods. Some obligations are relative: not to lie, unless truth-telling endangers our moral projects. It is obligatory under a range of circumstances where our moral projects are not jeopardised. But deontic logic is not S4, i.e., we don’t have $\Box p \to p$. Is this because we’re reading it wrong? Should be ‘ought to do $p$’ entailed by ‘over situations of this kind including this current one, ought to do $p$’.

Seems like people are expecting a graded deontic modality, allowing for different ranges of applicability.

The theory developed in the previous section enables us to model multi-modal information flow calculi, which feature modalities that are indexed in some way. The usual way to do so is to index them over a poset of security levels, and which is often (but not always) a lattice. (p. 22 of https://arxiv.org/abs/1809.07897)

Burnyeat (p. 21) on invariance rather than necessity.