Modal Logic and Modal Types08 Nov 2017
There is not a single modal logic, there are a large family of modal logics depending on what axioms there are.
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,
▢p is true as well. The latter is obviously problematic, as
is true in current world, doesn’t make it true in all accessible
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.
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  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
The paper  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.
- A Modal Analysis of Staged Computation, R. Davies et F. Pfenning, 2001.