% File: nk.elf

% Classical, Natural Deduction
nk : o -> type. 

nk_andi    : nk A -> nk B -> nk (A and B).
nk_andel   : nk (A and B) -> nk A.
nk_ander   : nk (A and B) -> nk B.
nk_impi    : (nk A -> nk B) -> nk (A imp B).
nk_impe    : nk (A imp B) -> nk A -> nk B.
nk_oril    : nk A -> nk (A or B).
nk_orir    : nk B -> nk (A or B).
nk_ore     : nk (A or B) -> (nk A -> nk C) -> (nk B -> nk C) -> nk C.
nk_noti    : ({p:o} nk A -> nk p) -> nk (not A).
nk_note    : nk (not A) -> {C:o} nk A -> nk C.
nk_truei   : nk true.
nk_falsee  : nk false -> nk C.
nk_foralli : ({a:i} nk (A a)) -> nk (forall A).
nk_foralle : nk (forall A) -> {T:i} nk (A T).
nk_existsi : {T:i} nk (A T) -> nk (exists A).
nk_existse : nk (exists A) -> ({a:i} nk (A a) -> nk C) -> nk C.

nk_dnotr   : nk A
     <- nk (not (not A)).  % double negation version of excluded middle

% 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 nk_dnotx_auto : forall* {A:o} exists {D:nk A -> nk (not not A)} true.
%prove 10 {} (nk_dnotx_auto D).

nk_dnotx = ([NK] (nk_noti [p:o] [u:nk (not A)] (nk_note u p NK))).