%%% Natural deduction for a fragment of intuitionistic logic
%%% Author: Frank Pfennig

%%% Individuals
i : type.	            %name i T.

%%% Propositions
o : type.		    %name o A.

imp    : o -> o -> o.	    %infix right 10 imp.
and    : o -> o -> o.	    %infix right 11 and.
true   : o.
or     : o -> o -> o.	    %infix right 11 or.
false  : o.
forall : (i -> o) -> o.
exists : (i -> o) -> o.

not : o -> o = [A:o] A imp false.

%%% Natural Deductions

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

impi    : (nd A -> nd B) -> nd (A imp B).
impe    : nd (A imp B) -> nd A -> nd B.
andi    : nd A -> nd B -> nd (A and B).
ande1   : nd (A and B) -> nd A.
ande2   : nd (A and B) -> nd B.
truei   : nd (true).
% no truee
ori1    : nd A -> nd (A or B).
ori2    : nd B -> nd (A or B).
ore     : nd (A or B) -> (nd A -> nd C) -> (nd B -> nd C) -> nd C.
% no falsei
falsee  : nd false -> nd C.
foralli : ({x:i} nd (A x)) -> nd (forall A).
foralle : nd (forall A) -> {T:i} nd (A T).
existsi : {T:i} nd (A T) -> nd (exists A).
existse : nd (exists A) -> ({x:i} nd (A x) -> nd C) -> nd C.

noti : (nd A -> nd false) -> nd (not A)
     = [D:nd A -> nd false] impi D.
note : nd (not A) -> nd A -> nd false
     = [D:nd (not A)] [E:nd A] impe D E.

%%% Verifying regular worlds
%block nd_hyp : some {A:o} block {u:nd A}.
%block nd_parm : block {x:i}.
%worlds (nd_hyp | nd_parm) (nd A).

%%% Local reductions

red : nd A -> nd A -> type.
impred : red (impe (impi D) E) (D E).
andred1 : red (ande1 (andi D E)) D.
andred2 : red (ande2 (andi D E)) E.
% no truered
orred1 : red (ore (ori1 D) E1 E2) (E1 D).
orred2 : red (ore (ori2 D) E1 E2) (E2 D).
% no falsered
forallred : red (foralle (foralli D) T) (D T).
existsred : red (existse (existsi T D) E) (E T D).

%%% A simple theorem

%theorem
trivI : exists {D:{A:o} nd (A imp A)}
	true.

%prove 2 {} (trivI D).