Modal logic

In this page we show how to encode modal logic in LF. Similarly to linear logic, the main idea here is to define a judgment that explicitly restricts the use of non-necessity assumptions (any assumption of a proof for a judgment that is not necessary).

The Encoding

Syntax

% Terms
%sort tm %.
%term unit tm %.
%term app %pi tm %-> tm %-> tm %.
%term lam %pi (%pi tm %-> tm) %-> tm %.
%term bx %pi tm %-> tm %.
%term letbox %pi tm %-> (%pi tm %-> tm) %-> tm %.
% Types
%sort tp %.
%term o tp %.
%term arrow %pi tp %-> tp %-> tp %.
%term box %pi tp %-> tp %.
%term dia %pi tp %-> tp %.

Local Judgment

The correct use of an assumption inside a proof term can be enforced by a local judgment. This jugment ensures that a variable is never used inside any term bx M that exists within its scope (we say that the variable is local).

%sort local {_ %pi tm %-> tm} %.

The simplest cases are the one for variables.

%term local/var local ([x] x) %.
%term local/closed local ([x] M) %.

A variable is local in an abstraction if it is local inside the abstraction’s body. Note that the abstraction’s argument (which must be local as well) is handled separately by the abstraction’s typing rule.

%term local/lam %pi (local ([x] lam ([y] N x y))) %<- ({y} local ([x] N x y)) %.

A variable is local in an application if it is local inside its subterms.

%term local/app %pi (local ([x] app (M x) (N x))) %<- (local ([x] M x)) %<- (local ([x] N x)) %.

The same idea applies to letbox.

%term local/letbox
  %pi (local ([x] letbox (M x) ([y] N x y)))
  %<- (local ([x] M x))
  %<- ({y} local ([x] N x y)) %.

Significantly, there is no rule for bx. Local variables are not permitted to appear within box terms.

Typing rules

The key idea introduced by our enconding of modal logic is that typing rules need to check (using the local judgment described above) that non-necessary assumptions are never used inside a term bx M . In our case, abstractions are the only terms that bind restricted (non-necessary) variables, and therefore the rule for letbox does not need to check whether its variable is local or not.

%sort of {_ tm} {_ tp} %.
%term of/unit of unit o %.
%term of/bx %pi (of (bx M) (box T)) %<- (of M T) %.
%term of/lam
  %pi (of (lam M) (arrow A B))
  %<- ({n tm} %pi (of n A) %-> (of (M n) B))
  %<- (local M) %.
%term of/letbox
  %pi (of (letbox N M) B)
  %<- (of N (box A))
  %<- ({n tm} %pi (of n A) %-> (of (M n) B)) %.
%term of/app %pi (of M (arrow T1 T2)) %-> (of N T1) %-> (of (app M N) T2) %.

>Source code for the encoding

Type Preservation

As an example, we can prove preservation using our encoding.

Evaluation Rules

First, we define the value judgment and evaluation rules.

%sort value {_ tm} %.
%term value/unit value unit %.
%term value/lam value (lam M) %.
%term value/bx %pi (value (bx M)) %<- (value M) %.
%%%%%% Evaluation rules %%%%%%
%sort step {_ tm} {_ tm} %.
%term step/beta %pi (step (app (lam N) M) (N M)) %<- (value M) %.
%term step/app1 %pi (step (app M N) (app M1 N)) %<- (step M M1) %<- (value N) %.
%term step/app2 %pi (step (app M N) (app M N1)) %<- (step N N1) %.
%term step/bx %pi (step (bx M) (bx N)) %<- (step M N) %.
%term step/letbox %pi (step (letbox M N) (letbox M' N)) %<- (step M M') %.
%term step/letbox/beta %pi (step (letbox (bx M) N) (N M)) %<- (value M) %.

Type Preservation Proof

%sort step-type {_ of M A} {_ step M N} {_ of N A} %.
%mode step-type %in %in %out %.
%term step-type/beta step-type (of/app (of/lam LN P) OM) (%the (step (app (lam N) M) (N M)) (step/beta _)) (P M OM) %.
%term step-type/app1
  %pi (step-type (of/app OM ON) (step/app1 _ R) (of/app OM1 ON))
  %<- (step-type OM R OM1) %.
%term step-type/app2
  %pi (step-type (of/app ON OM) (step/app2 R) (of/app ON OM1))
  %<- (step-type OM R OM1) %.
%term step-type/bx %pi (step-type (of/bx PM) (step/bx S) (of/bx PN)) %<- (step-type PM S PN) %.
%term step-type/letbox
  %pi (step-type (of/letbox ON OM) (step/letbox R) (of/letbox ON OM1))
  %<- (step-type OM R OM1) %.
%term step-type/letbox/beta step-type (of/letbox P (of/bx OM)) (step/letbox/beta _) (P M OM) %.
%worlds () (step-type _ _ _) %.
%total (R) (step-type R _ _) %.

>Complete Source code

check=true>STELF Output