% File: nj.elf

% Intuitionistic, Natural Deduction
nj : o -> type.

nj_andi    : nj A -> nj B -> nj (A and B).
nj_andel   : nj (A and B) -> nj A.
nj_ander   : nj (A and B) -> nj B.
nj_impi    : (nj A -> nj B) -> nj (A imp B).
nj_impe    : nj (A imp B) -> nj A -> nj B.
nj_oril    : nj A -> nj (A or B).
nj_orir    : nj B -> nj (A or B).
nj_ore     : nj (A or B) -> (nj A -> nj C) -> (nj B -> nj C) -> nj C.
nj_noti    : ({p:o} nj A -> nj p) -> nj (not A).
nj_note    : nj (not A) -> {C:o} nj A -> nj C.
nj_truei   : nj true.
nj_falsee  : nj false -> nj C.
nj_foralli : ({a:i} nj (A a)) -> nj (forall A).
nj_foralle : nj (forall A) -> {T:i} nj (A T).
nj_existsi : {T:i} nj (A T) -> nj (exists A).
nj_existse : nj (exists A) -> ({a:i} nj (A a) -> nj C) -> nj C.

% In intuitionistic/classical logic we have the following derivation
% of A :- (not not A)

%    --------- u
%      not A        A [hyp]
%    ---------------------- note(p)
%                p
%          ----------- noti^p^u
%          (not not A)

%theorem nj_dnotx_auto : forall* {A:o} exists {D:nj A -> nj (not not A)} true.
%prove 10 {} (nj_dnotx_auto D).

nj_dnotx = ([NJ] (nj_noti [p:o] [u:nj (not A)] (nj_note u p NJ))).

% Lemma 1: 
% In intuitionistic logic we have the 
% following derivation of (not not not A):- (not A)

%         ------------------- u
%                  A
%         ------------------- dnotx
%                - - A                   - - - A [hyp] 
%          ------------------------------------------- note(q) 
%                           q 
%                 ------------------ noti^q^u 
%                          - A 
% represented in Elf by the definition nj_triple_neg_red given by
% [w:nj (not (not (not A)))] (nj_noti ([q:o] [u:nj A] (nj_note w q (noti ([p:o] [v:nj (not A)] (note v p u))))))

% %theorem nj_triple_neg_red_auto : forall* {A:o} forall {D:nj (not not not A)} exists {D':nj (not A)} true.
% %prove 7 {} (nj_triple_neg_red_auto D D').

nj_triple_neg_red = ([NJ] 
                       (nj_noti [q:o] [u:nj A] 
                          (nj_note NJ q (nj_dnotx u)))).

% Lemma 2:
% In intuitionistic logic we have the following derivation
% of (not not false) :- C

%   -------- u
%    false
%   -------- falsee
%      p
%   --------- noti^p^u
%   not false            not not false [hyp]
%   ------------------------------------------ note(C)
%               C

%theorem nj_dneg_falser_auto : forall* {A:o} exists {D:nj (not not false) -> {C:o} nj C} true.
%prove 10 {} (nk_dnotx_auto D).

nj_dneg_falser = ([NJ1] [C] (nj_note 
                               NJ1 C
                               (nj_noti ([p] [u:nj false] 
                                  (nj_falsee u))))).