Inference Rules of Classical Linear Logic

%%% Cut-Free Classical Linear Sequent Calculus
%%% Author: Frank Pfenning
%%%
%%% The three rules for cut can also be formulated and are
%%% given in a comment at the end

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

%% Axioms

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

%% Multiplicative Connectives

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 #).

%% Additive Connectives

andr : ((pos A -o #) & (pos B -o #))
	-o (pos (A and B) -o #).

andl1 : (neg A -o #)
	 -o (neg (A and B) -o #).

andl2 : (neg B -o #)
	 -o (neg (A and B) -o #).

topr :  -o (pos (top) -o #).

% no topl

%% Involution

perpr : (neg A -o #)
	 -o (pos (perp A) -o #).

perpl : (pos A -o #)
	 -o (neg (perp A) -o #).

%% Modal Operators

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

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

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

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

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

?d : (pos A -o #)
      -o (pos? A -> #).

%{
%% Cuts

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

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

cut? : (neg? A -> #)
	-o (pos A -o #)
	-> #.
}%

Frank Pfenning