Annotated Linear Minimal Natural Deduction

%%% Minimal Linear Natural Deduction
%%% Annotated (elim, intro)
%%% Author: Frank Pfenning

elim : o -> type. % Elimination Deductions from Hypotheses (forward)
intro : o -> type. % Introductory Deductions from Conclusions (backward)
%name elim E
%name intro I

%% Coercions

e2i : (elim A -o intro A).   % corresponds to axioms
i2e : (intro A -o elim A).   % corresponds to cut

%% Multiplicative Connectives

impi' : (elim A -o intro B)
	 -o intro (A imp B).

impe' : intro A
	 -o elim (A imp B)
	 -o elim B.

timesi' : intro A 
	   -o intro B
	   -o intro (A times B).

timese' : (elim A -o elim B -o intro C)
	   -o (elim (A times B) -o intro C).

onei' : intro one.

onee' : intro C
	 -o (elim one -o intro C).

% no par (multiplicative disjunction)

% no bot (multiplicative falsehood)

%% Additive Connectives

% no wave (additive implication)

withi' : (intro A & intro B)
	  -o intro (A with B).

withe1' : elim (A with B)
	   -o elim A.

withe2' : elim (A with B)
	   -o elim B.

topi' : <T>
	 -o intro (top).

% no tope

plusi1' : intro A
	   -o intro (A plus B).

plusi2' : intro B
	   -o intro (A plus B).

pluse' : ((elim A -o intro C) & (elim B -o intro C))
	  -o (elim (A plus B) -o intro C).

% no zeroi

zeroe' : <T>
	  -o (elim (zero) -o intro C).

%% No negation

%% Quantifiers

foralli' : ({a:i} intro (A a))
	    -o intro (forall A).

foralle' : {T:i} elim (forall A)
	    -o elim (A T).

existsi' : {T:i} intro (A T)
	    -o intro (exists A).

existse' : ({a:i} elim (A a) -o intro C)
	    -o (elim (exists A) -o intro C).

%% Exponentials

!i' : intro A
       -> intro (! A).

!e' : (elim A -> intro C)
       -o (elim (! A) -o intro C).

Frank Pfenning