% Kolmogorov translation

%sig JUDGMENTS = { 
   o : type.
   true : o -> type.
}.	        

%sig IMP = { 
   %struct J : JUDGMENTS %open o true.
  =>: o -> o -> o.    %infix left 10 =>.
  =>I : (true A -> true B) -> true (A => B).
  =>E : true (A => B) -> true A -> true B.
}.

%sig NEG = {
   %struct J : JUDGMENTS %open o true.
  ~ : o -> o.
  n =  [p] (~ (~ p)).
  ~I : ({p} true A -> true p) -> true (~ A).
  ~E : true (~ A) -> true A -> true B.
  ~~I : true A -> true (n A) = [D] (~I [p:o] [u: true (~ A)] (~E u D)).
}.

%sig IL = { 
   %struct J : JUDGMENTS %open o true.
   %struct I : IMP  = { %struct J := J.} %open => =>I =>E.
   %struct N : NEG  = { %struct J := J.} %open ~ n ~I ~E ~~I. 
}.

%sig CL = {
   %struct IL : IL %open o true => =>I =>E ~ n ~I ~E ~~I.
   exm : true (~ (~ A) => A). 
}.

%view KOLMJ : JUDGMENTS -> IL = {
  o := o.
  true :=  [x] true (n x).
}.

%view KOLMN : NEG -> IL = {
  %struct  J := KOLMJ.				
  ~ := [x] ~ x.
  ~I := [A][D] ~I [q][u] ~E (D (~ A) u) u.
  ~E := [A][C][D][E] ~I [p][u] ~E D E .
}.

%view KOLMI : IMP -> IL = {
  %struct  J := KOLMJ.				
  => := [x][y] ((n x) => (n y)).
  =>I := [A][B][D] ~~I (=>I D).
  =>E := [A][B][D][E] ~I [p][u] ~E D (~I [q][v] ~E (=>E v E) u).
}.

%view KOLMIL : IL -> IL = {
  %struct J := KOLMJ.
  %struct I := KOLMI.
  %struct N := KOLMN.
}.

%view KOLM : CL -> IL = {
  %struct IL := KOLMIL.
  exm :=  [A] ~I [p] [u] ~E u (=>I [u] ~I [p] [v] ~E u (~I [q][w] ~E w v)).
}.

%view KOLMJinv : JUDGMENTS -> CL = {
  o := o.
  true :=  [x] true x.
}.

%view KOLMNinv : NEG -> CL = {
  %struct J := KOLMJinv.				      
  ~ := [x] ~ x.
  ~I := [A][D] ~I D.
  ~E := [A][C][D][E] ~E D E.
}.


%view KOLMIinv : IMP -> CL = {
  %struct J := KOLMJinv.
  => := [x][y] x => y.
  =>I := [A][B][D] =>I D.
  =>E := [A][B][D][E] =>E D E.
}.

%view KOLMILinv : IL -> CL = {
  %struct J := KOLMJinv.
  %struct I := KOLMIinv.
  %struct N := KOLMNinv.
}.