// // // Implementing Kolmogorov's translation on propositional logic // // // February 2005: It is completed by Sa Cui and Hongwei Xi // January 2007: It is ported to ATS/Geizella by Hongwei Xi // March 5th, 2008: // It is verified by ATS/Anairiats (without any changes being made). (* ****** ****** *) // Infix operators infixl land // left associative infixl lor // left associative infixr limp // right associative // Types for formulas datasort form = | ltrue | lfalse | lnot of form | land of (form, form) | lor of (form, form) | limp of (form, form) // Types for contexts datasort forms = nil | :: of (form, forms) // [IN (A, G)] : The formula A is in the context G dataprop IN (form, forms) = | {G:forms} {A:form} INone (A, A :: G) | {G:forms} {A,B:form} INshi (A, B :: G) of IN (A, G) // Double negation stadef dneg (f: form): form = lnot (lnot f) // KOLM (A, A'): Kolmogrov's translation dataprop KOLM (form, form, int) = | KOLMfalse (lfalse, dneg (lfalse), 0) | KOLMtrue (ltrue, dneg (ltrue), 0) | {A,A':form} {n:nat} KOLMnot (lnot A, dneg (lnot (dneg A')), n+1) of KOLM (A, dneg A', n) | {A,A',B,B':form} {n1,n2:nat} KOLMand (A land B, dneg ((dneg A') land (dneg B')), n1+n2+1) of (KOLM (A, dneg A', n1), KOLM (B, dneg B', n2)) | {A,A',B,B':form} {n1,n2:nat} KOLMor (A lor B, dneg ((dneg A') lor (dneg B')), n1+n2+1) of (KOLM (A, dneg A', n1), KOLM (B, dneg B', n2)) | {A,A',B,B':form} {n1,n2:nat} KOLMimp (A limp B, dneg ((dneg A') limp (dneg B')), n1+n2+1) of (KOLM (A, dneg A', n1), KOLM (B, dneg B', n2)) propdef KOLM0 (A:form, A':form) = [n:nat] KOLM (A, A', n) dataprop FMEQ (form, form) = {A:form} FMEQ (A, A) prfun fmeq {A,A',A'':form} {n1,n2:nat} .. (pf1: KOLM (A, A', n1), pf2: KOLM (A, A'', n2)) : FMEQ (A', A'') = begin case+ (pf1, pf2) of | (KOLMfalse (), KOLMfalse ()) => FMEQ | (KOLMtrue (), KOLMtrue ()) => FMEQ | (KOLMnot pf11, KOLMnot pf21) => let prval FMEQ () = fmeq (pf11, pf21) in FMEQ () end | (KOLMand (pf11, pf12), KOLMand (pf21, pf22)) => let prval FMEQ () = fmeq (pf11, pf21) prval FMEQ () = fmeq (pf12, pf22) in FMEQ () end | (KOLMor (pf11, pf12), KOLMor (pf21, pf22)) => let prval FMEQ () = fmeq (pf11, pf21) prval FMEQ () = fmeq (pf12, pf22) in FMEQ () end | (KOLMimp (pf11, pf12), KOLMimp (pf21, pf22)) => let prval FMEQ () = fmeq (pf11, pf21) prval FMEQ () = fmeq (pf12, pf22) in FMEQ () end end // end of [fmeq] (* prfun KOLMfun {A:form}: [A':form] KOLM (A, A') = scase A of | lfalse => dneg (A) | ltrue => dneg (A) | lnot A => ... | land of (form, form) | lor of (form, form) | limp of (form, form) *) // Existence of Kolmogorov's translation // Given a formula A, there exists A', such that KOLM (A, A') extern prval KOLMfun : {A:form}[A':form] KOLM0 (A, dneg A') // Kolmogrov's translation on contexts dataprop KOLMS (forms, forms, int) = | KOLMSnil (nil, nil, 0) | {G,G':forms} {A,A':form} {n:nat} KOLMScons (A :: G, dneg A' :: G', n+1) of (KOLM0 (A, dneg A'), KOLMS (G, G',n)) propdef KOLMS0 (G:forms, G':forms) = [n:nat] KOLMS (G, G', n) // Classical natural deduction dataprop NK (forms, form, int) = | {G:forms} {A:form} {n:nat} NKfalse (G, A, n+1) of NK (G, lfalse, n) | {G:forms} NKtrue (G, ltrue, 0) | {G:forms} {A:form} NKhyp (G, A, 0) of IN (A, G) | {G:forms} {A,B:form} {n1,n2:nat} NKandi (G, A land B, n1+n2+1) of (NK (G, A, n1), NK (G, B, n2)) | {G:forms} {A,B:form} {n:nat} NKandel (G, A, n+1) of NK(G, A land B, n) | {G:forms} {A,B:form} {n:nat} NKander (G, B, n+1) of NK(G, A land B, n) | {G:forms} {A,B:form} {n:nat} NKoril (G, A lor B, n+1) of NK (G, A, n) | {G:forms} {A,B:form} {n:nat} NKorir (G, A lor B, n+1) of NK (G, B, n) | {G:forms} {A,B,C:form} {n1,n2,n3:nat} NKore (G, C, n1+n2+n3+1) of (NK (G, A lor B, n1), NK (A :: G, C, n2), NK (B :: G, C, n3)) | {G:forms} {A,B:form} {n:nat} NKimpi (G, A limp B, n+1) of NK (A :: G, B, n) | {G:forms} {A,B:form} {n1,n2:nat} NKimpe (G, B, n1+n2+1) of (NK (G, A limp B, n1), NK (G, A, n2)) | {G:forms} {A:form} {n:nat} NKnoti (G, lnot A, n+1) of NK (A :: G, lfalse, n) | {G:forms} {A:form} {n1,n2:nat} NKnote (G, lfalse, n1+n2+1) of (NK (G, lnot A, n1), NK (G, A, n2)) | {G:forms} {A:form} {n:nat} NKdneg (G, A, n+1) of NK (G, lnot (lnot A), n) propdef NK0 (G:forms, A:form) = [n:nat] NK (G, A, n) // Intuitionistic Natural Deduction dataprop NJ (forms, form, int) = | {G:forms} {A:form} {n:nat} NJfalse (G, A, n+1) of NJ (G, lfalse, n) | {G:forms} NJtrue (G, ltrue, 0) | {G:forms} {A:form} NJhyp (G, A, 0) of IN (A, G) | {G:forms} {A,B:form} {n1,n2:nat} NJandi (G, A land B, n1+n2+1) of (NJ (G, A, n1), NJ (G, B, n2)) | {G:forms} {A,B:form} {n:nat} NJandel (G, A, n+1) of NJ(G, A land B, n) | {G:forms} {A,B:form} {n:nat} NJander (G, B, n+1) of NJ(G, A land B, n) | {G:forms} {A,B:form} {n:nat} NJoril (G, A lor B, n+1) of NJ (G, A, n) | {G:forms} {A,B:form} {n:nat} NJorir (G, A lor B, n+1) of NJ (G, B, n) | {G:forms} {A,B,C:form} {n1,n2,n3:nat} NJore (G, C, n1+n2+n3+1) of (NJ (G, A lor B, n1), NJ (A :: G, C, n2), NJ (B :: G, C, n3)) | {G:forms} {A,B:form} {n:nat} NJimpi (G, A limp B, n+1) of NJ (A :: G, B, n) | {G:forms} {A,B:form} {n1,n2:nat} NJimpe (G, B, n1+n2+1) of (NJ (G, A limp B, n1), NJ (G, A, n2)) | {G:forms} {A,B:form} {n:nat} NJnoti (G, lnot A, n+1) of NJ (A :: G, lfalse, n) | {G:forms} {A:form} {n1,n2:nat} NJnote (G, lfalse, n1+n2+1) of (NJ (G, lnot A, n1), NJ (G, A, n2)) propdef NJ0 (G:forms, A:form) = [n:nat] NJ (G, A, n) // Given a KOLMS (G, G', n) on contexts with a metric, and a prop IN (A, G), // there exists a formula A', such that KOLM (A, A') and IN (A', G'). prfun proposition10 {G,G':forms} {A:form} {n:nat} .. (ks: KOLMS (G, G',n), i: IN (A, G)) : [A':form] (KOLM0 (A, dneg A'), IN (dneg A', G')) = begin case+ i of | INone () => let prval KOLMScons (k, ks) = ks in (k, INone ()) end | INshi i' => let prval KOLMScons (k, ks) = ks prval (k, i') = proposition10 (ks, i') in (k, INshi i') end end // end of [proposition10] // Double negation rule prfn proposition20 {G:forms} {A:form} (): NJ0 (G, A limp (lnot (lnot A))) = NJimpi (NJnoti (NJnote (NJhyp INone, NJhyp (INshi INone)))) prfn proposition21 {G:forms} {A:form} (pf: NJ0 (G, A)): NJ0 (G, lnot (lnot A)) = NJimpe (proposition20 (), pf) // Double false rule prfn proposition30 {G:forms} (): NJ0 (G, (lnot (lnot lfalse)) limp lfalse) = NJimpi (NJnote ((NJhyp INone), NJnoti (NJhyp INone))) prfn proposition31 {G:forms} (pf: NJ0 (G, dneg lfalse)): NJ0 (G, lfalse) = NJimpe (proposition30 (), pf) // not not not R prfn proposition35 {G:forms} {A:form} () : NJ0 (G, (lnot (dneg A)) limp (lnot A)) = let stadef G1:forms = lnot (dneg A) :: G prval pf = proposition21 (NJhyp (INone {G1} {A} ())) in NJimpi (NJnoti (NJnote (NJhyp (INshi INone), pf))) end // end of [proposition35] prfn proposition36 {G:forms} {A:form} (pf: NJ0 (G, lnot (dneg A))): NJ0 (G, lnot A) = NJimpe (proposition35 (), pf) (***********************************************************************************) propdef SUP (G2:forms, G1:forms) = {A: form} IN (A, G1) - IN (A, G2) // Weakening prfn proposition40 {G1,G2:forms} {A:form} (f: SUP (G2, G1)) : SUP (A :: G2, G1) = lam i => INshi (f i) // Exchange prfn proposition41 {G1,G2:forms} {A1,A2:form} (f: SUP (G2, G1)): SUP (A1 :: A2 :: G2, A2 :: A1 :: G1) = begin lam i => case+ i of | INone () => INshi (INone) | INshi (INone ()) => INone | INshi (INshi i) => INshi (INshi (f i)) end // end of [proposition41] // Shift prfn proposition42 {G1,G2:forms} {A:form} (f: SUP (G2, G1)): SUP (A :: G2, A :: G1) = begin lam i => case+ i of | INone () => INone | INshi i => INshi (f i) end // end of [proposition42] // prfun proposition43 {G1,G2:forms} {A:form} {n:nat} .. (f: SUP (G2, G1)) (pf: NJ (G1, A, n)): NJ (G2, A, n) = begin case+ pf of | NJhyp i => NJhyp (f i) | NJtrue () => NJtrue | NJfalse pf => NJfalse (proposition43 f pf) | NJandi (pf1, pf2) => NJandi (proposition43 f pf1, proposition43 f pf2) | NJandel pf => NJandel (proposition43 f pf) | NJander pf => NJander (proposition43 f pf) | NJoril pf => NJoril (proposition43 f pf) | NJorir pf => NJorir (proposition43 f pf) | NJore (pf, pf1, pf2) => NJore ( proposition43 f pf , proposition43 (proposition42 f) pf1 , proposition43 (proposition42 f) pf2 ) // end of [NJore] | NJimpi pf => NJimpi (proposition43 (proposition42 f) pf) | NJimpe (pf1, pf2) => NJimpe (proposition43 f pf1, proposition43 f pf2) | NJnoti pf => NJnoti (proposition43 (proposition42 f) pf) | NJnote (pf1, pf2) => NJnote (proposition43 f pf1, proposition43 f pf2) end // end of [proposition43] // Weakening rule prfn proposition44 {G:forms} {A,A':form} (pf: NJ0 (G, A)) : NJ0 (A' :: G, A) = (proposition43 (proposition40 (lam i => i)) pf) // Exchanging rule prfn proposition45 {G:forms} {A1,A2,A3:form} (pf: NJ0 (A1 :: A2 :: G, A3)) : NJ0 (A2 :: A1 :: G, A3) = (proposition43 (proposition41 (lam i => i)) pf) (****************************************************************************************) // Soundness: // whenever a formula A is provable in NK, its translation A' is provable in NJ prfun trans {G,G':forms} {A:form} {n:nat} .. (ks: KOLMS0 (G, G'), kpf: NK (G, A, n)) : [A':form] (KOLM0 (A, dneg A'), NJ0 (G', dneg A')) = begin case+ kpf of | NKhyp i => let prval (k, i) = proposition10 (ks, i) in (k, NJhyp i) end | NKtrue () => (KOLMtrue, proposition21 NJtrue) | NKfalse kpf => let prval (KOLMfalse (), jpf) = trans (ks, kpf) prval k' = KOLMfun {...} in (k', NJfalse (proposition31 jpf)) end | NKandi (kpf1, kpf2) => let prval (k1, jpf1) = trans (ks, kpf1) prval (k2, jpf2) = trans (ks, kpf2) in (KOLMand (k1, k2), proposition21 (NJandi (jpf1, jpf2))) end | NKandel kpf => let prval (KOLMand (k1, k2), jpf) = trans (ks, kpf) prval pf1 = NJhyp (INshi INone) prval pf2 = NJandel (NJhyp INone) prval pf3 = NJnote (pf2, pf1) prval pf4 = NJnoti pf3 prval pf5 = NJnote (proposition44 jpf, pf4) prval pf6 = NJnoti pf5 in (k1, pf6) end | NKander kpf => let prval (KOLMand (k1, k2), jpf) = trans (ks, kpf) prval pf1 = NJhyp (INshi INone) prval pf2 = NJander (NJhyp INone) prval pf3 = NJnote (pf2, pf1) prval pf4 = NJnoti pf3 prval pf5 = NJnote (proposition44 jpf, pf4) prval pf6 = NJnoti pf5 in (k2, pf6) end | NKoril kpf => let prval (k1, jpf) = trans (ks, kpf) prval k2 = KOLMfun {...} in (KOLMor (k1, k2), proposition21 (NJoril jpf)) end | NKorir kpf => let prval (k2, jpf) = trans (ks, kpf) prval k1 = KOLMfun {...} in (KOLMor (k1, k2), proposition21 (NJorir jpf)) end | NKore {..} {A1,A2,A3} {..} (kpf1, kpf2, kpf3) => let prval [A':form] (KOLMor (k11, k12), jpf1) = trans (ks, kpf1) prval (k2, jpf2) = trans (KOLMScons (k11, ks), kpf2) prval (k3, jpf3) = trans (KOLMScons (k12, ks), kpf3) prval FMEQ () = fmeq (k2, k3) prval [A3':form] k4 = KOLMfun {A3} prval jpf4 = proposition45 (proposition44 jpf2) prval jpf4 = proposition45 (proposition44 jpf4) prval jpf5 = proposition45 (proposition44 jpf3) prval jpf5 = proposition45 (proposition44 jpf5) prval FMEQ () = fmeq (k2, k4) prval pf1 = NJore (NJhyp (INone {lnot A3' :: G'} {A'}), jpf4, jpf5) prval pf2 = NJnote (pf1, NJhyp (INshi INone)) prval pf3 = NJnoti pf2 prval pf4 = NJnote (proposition44 jpf1, pf3) prval pf5 = NJnoti pf4 in (k4, pf5) end | NKnoti kpf => let (* kpf: NK (A::G, lfalse) *) prval k1 = KOLMfun {...} prval (KOLMfalse (), jpf) = trans (KOLMScons (k1, ks), kpf) prval pf1 = proposition31 jpf prval pf2 = NJnoti pf1 prval pf3 = proposition21 pf2 in (KOLMnot k1, pf3) end | NKnote (kpf1, kpf2) => let prval (KOLMnot k1, jpf1) = trans (ks, kpf1) prval (k2, jpf2) = trans (ks, kpf2) prval FMEQ () = fmeq (k1, k2) prval jpf1' = (proposition36) jpf1 prval pf1 = NJnote (jpf1', jpf2) prval pf2 = proposition21 pf1 in (KOLMfalse(), pf2) end | NKimpi kpf => let prval k1 = KOLMfun {...} prval (k2, jpf) = trans (KOLMScons (k1, ks), kpf) in (KOLMimp (k1, k2), proposition21 (NJimpi jpf)) end | NKimpe {..} {A1,A2} {..} (kpf1, kpf2) => let prval [A':form] (KOLMimp (k1, k2), jpf1) = trans (ks, kpf1) prval (k3, jpf2) = trans (ks, kpf2) prval FMEQ () = fmeq (k1, k3) prval [A2':form] k4 = KOLMfun {A2} prval pf0 = proposition44 (proposition44 jpf2) prval FMEQ () = fmeq (k2, k4) prval pf1 = NJimpe (NJhyp (INone {lnot A2' :: G'} {A'}), pf0) prval pf2 = NJnote (pf1, NJhyp (INshi INone)) prval pf3 = NJnoti pf2 prval pf4 = NJnote (proposition44 jpf1, pf3) prval pf5 = NJnoti pf4 in (k2, pf5) end | NKdneg kpf => let prval (KOLMnot (KOLMnot k), jpf) = trans (ks, kpf) prval pf = proposition36 (proposition36 (proposition36 jpf)) in (k, pf) end end // end of [trans] (* ****** ****** *) (* end of [KolmogorovTrans.dats] *)