# Modal Logic and Modal Types

08 Nov 2017There is not a single modal logic, there are a large family of modal logics depending on what axioms there are.

## Necessitation rule

Every modal logic includes the *necessitation rule* (N) and *distribution
axiom* (K), which together forms the minimum modal logic system K.

The distribution axiom is as follows, there’s no controversy here.

⊢ ▢(p -> q) -> (▢p -> ▢q)

Some confusion may arise with the necessitation rule. The correct formulation is as follows:

if ⊢ p, then ⊢ ▢p.

Any attempt to simplify the formulation to `⊢ p -> ▢p`

will cause
problems, as the latter means completely different things. The
necessitation rule says that if `p`

is *unconditionally* true, then
`▢p`

is also *unconditionally* true. The latter says, if `p`

is true,
then `▢p`

is true as well. The latter is obviously problematic, as `p`

is true in current world, doesn’t make it true in all accessible
worlds.

System S4 adds two axioms to system K:

- T: ⊢ ▢p -> p
- 4: ⊢ ▢p -> ▢▢p

The two axioms correspond to reflexivity and transitivity of the accessibility relation in Kripke semantics.

## Subject reduction

A variant of the nessitation rule says that *we can infer ▢p if all
the hypothesis used in inferring p is of the form ▢q*. This variant
works well in logic, except proof simplification doesn’t observe
subject reduction, which causes problem in type systems.

According to *Curry-Howard correspondence*, types correspond to
propositions, terms correspond to proofs, and proof simplification
correspond to evaluation. The problem with proof simplification will
yield an unsound type system.

The problem can be demonstrated by the following example:

```
b: B, f: B -> ▢A ⊢ (\x: ▢A. box x) (f b) : ▢▢A
b: B, f: B -> ▢A ⊢ box (f b) : ▢▢A
```

As can be seen from the above, after one evaluation step, the term cannot be type checked anymore.

That’s the main motivation in [1] to distinguish between valid propositions and true propositions, which leads to a two-environment type system. The two most important typing rules in the system are as follows:

```
Δ; Ø ⊢ t: T
-----------------
Δ; Γ ⊢ box t: ▢T
Δ; Γ ⊢ t1: ▢T (Δ, x:T); Γ ⊢ t2: U
------------------------------------------
Δ; Γ ⊢ let box x = t1 in t2: U
```

## Sound Call-by-value system

In a call-by-value setting, the previous problem cannot occur. That implies there is no need to distinguish between true and valid propositions. A simpler system can be formulated with just one environment:

```
▢Γ ⊢ t : T
---------------
Γ ⊢ box t : ▢T
Γ ⊢ t : ▢T
---------------
Γ ⊢ unbox t : T
```

In the above, ▢Γ means only keep variables of modal types in the environment. Local soundness still holds:

```
Γ ⊢ unbox (box t): T ~~~~> Γ ⊢ t: T
```

However, local completeness doesn’t hold for naive encoding:

```
Γ ⊢ t: ▢T ~~~~> Γ ⊢ box (unbox t): ▢T
```

Local completeness holds with the following trick:

```
Γ ⊢ t: ▢T ~~~~> Γ ⊢ (\x:▢T. box (unbox x)) t: ▢T
```

## Kripke-style system

The paper [1] also introduces a Kripke-style type system, where the relation to kripke semantics is more direct. But the system is more verbose, as a stack of environments are required to modal the worlds.

## Reference

*A Modal Analysis of Staged Computation*, R. Davies et F. Pfenning, 2001.