Minimal Linear Natural Deduction

%%% Minimal Linear Natural Deduction
%%% Author: Frank Pfenning

nd : o -> type.  % Natural Deductions
%name nd D

%% Multiplicative Connectives

impi : (nd A -o nd B)
	-o nd (A imp B).

impe : nd A
	-o nd (A imp B)
	-o nd B.

timesi : nd A 
	  -o nd B
	  -o nd (A times B).

timese : (nd A -o nd B -o nd C)
	  -o (nd (A times B) -o nd C).

onei : nd one.

onee : nd C
	-o (nd one -o nd C).

% no par (multiplicative disjunction)

% no bot (multiplicative falsehood)

%% Additive Connectives

% no wave (additive implication)

withi : nd A & nd B
         -o nd (A with B).

withe1 : nd (A with B)
	  -o nd A.

withe2 : nd (A with B)
	  -o nd B.

topi : <T>
	-o nd (top).

% no tope

plusi1 : nd A
	  -o nd (A plus B).

plusi2 : nd B
	  -o nd (A plus B).

pluse : (nd A -o nd C) & (nd B -o nd C)
         -o (nd (A plus B) -o nd C).

% no zeroi

zeroe : <T>
	 -o (nd (zero) -o nd C).

%% No negation

%% Quantifiers

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

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

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

existse : ({a:i} nd (A a) -o nd C)
	   -o (nd (exists A) -o nd C).

%% Exponentials

!i : nd A
      -> nd (! A).

!e : (nd A -> nd C)
      -o (nd (! A) -o nd C).

Frank Pfenning