Minimal Linear Sequent Calculus

%%% Minimal Linear Sequent Calculus
%%% Author: Frank Pfenning

# : type.         % Token (for derivations)
neg!: o -> type.  % Modal Hypotheses (far left)
neg : o -> type.  % Hypotheses (left)
pos : o -> type.  % Conclusions (right)
%name # D
%name neg! N!
%name neg N
%name pos P

%% Axioms

axiom : (neg A -o pos A -o #).

%% Multiplicative Connectives

impr : (neg A -o pos B -o #)
	-o (pos (A imp B) -o #).

impl : (pos A -o #)
	-o (neg B -o #)
	-o (neg (A imp B) -o #).

timesr : (pos A -o #)
	  -o (pos B -o #)
	  -o (pos (A times B) -o #).

timesl : (neg A -o neg B -o #)
	  -o (neg (A times B) -o #).

oner : (pos one -o #).

onel : #
	-o (neg one -o #).

% no par (multiplicative disjunction)

% no bot (multiplicative falsehood)

%% Additive Connectives

% no wave (additive implication)

withr : (pos A -o #) & (pos B -o #)
         -o (pos (A with B) -o #).

withl1 : (neg A -o #)
	  -o (neg (A with B) -o #).

withl2 : (neg B -o #)
	  -o (neg (A with B) -o #).

topr : <T>
	-o (pos (top) -o #).

% no topl

plusr1 : (pos A -o #)
	  -o (pos (A plus B) -o #).

plusr2 : (pos B -o #)
	  -o (pos (A plus B) -o #).

plusl : (neg A -o #) & (neg B -o #)
         -o (neg (A plus B) -o #).

% no zeror

zerol : <T>
	 -o (neg (zero) -o #).

%% No negation

%% Quantifiers

forallr : ({a:i} pos (A a) -o #)
	   -o (pos (forall A) -o #).

foralll : {T:i} (neg (A T) -o #)
	   -o (neg (forall A) -o #).

existsr : {T:i} (pos (A T) -o #)
	   -o (pos (exists A) -o #).

existsl : ({a:i} neg (A a) -o #)
	   -o (neg (exists A) -o #).

%% Exponentials

!r : (pos A -o #)
      -> (pos (! A) -o #).

!l : (neg! A -> #)
      -o (neg (! A) -o #).

!d : (neg A -o #)
      -o (neg! A -> #).

%% Cuts

cut : (pos A -o #)
       -o (neg A -o #)
       -o #.

cut! : (pos A -o #)
	-> (neg! A -> #)
	-o #.

Frank Pfenning