/* logic.j -- an axiomatization of wffs, prfs, and ded. Because of certain syntactic conventions/restrictions of Jape, the following list shows new names that are given to certain objects in our axiomatization. The rest remain the same: When we usually write ... we now write ... :=> Imp [] nil [x] {x} T Truth F Falsity */ /* The following are standard Jape modules that provide support for logical reasoning, and equational rewriting: */ USE "aipc.j" USE "eq.j" USE "hci.j" /* fixity declarations: */ CONSTANT nil OUTFIX { } INFIX 15000 15000 union INFIX 10000 10000 without INFIX 5000 5000 subset INFIX 5000 5000 notin INFIX 5000 5000 in /* A simple theory of sets (to be used for handling manipulations involving hypotheses: */ THEORY Sets (xs,ys,zs,x,y) RULES union ARE nil union ys = ys AND ys union nil = ys RULES notin ARE x notin nil AND FROM ~(x=y) INFER x notin {y} AND FROM x notin xs AND x notin ys INFER x notin xs union ys RULES in ARE FROM x=y INFER x in {y} AND FROM x in xs INFER x in xs union ys AND FROM x in ys INFER x in xs union ys RULES subset ARE nil subset ys AND FROM x in ys INFER {x} subset ys AND FROM xs subset zs AND ys subset zs INFER xs union ys subset zs AND FROM xs subset ys INFER xs subset ys union zs AND FROM xs subset zs INFER xs subset ys union zs RULES without ARE nil without y = nil AND FROM x=y INFER {x} without y = nil AND FROM ~(x=y) INFER {x} without y = {x} AND xs union ys without y = (xs without y) union (ys without y) RULE Setinduction(E, FRESH xs, FRESH ys, FRESH x, FRESH xyzzy, P) WHERE VAR x, xs, ys AND FRESH x, xs, ys AND SAFE P[xyzzy\E], P[xyzzy\nil], P[xyzzy\xs], P[xyzzy\ys] FROM P[xyzzy \ nil] AND P[xyzzy \ {x}] AND P[xyzzy \ xs], P[xyzzy \ ys] |- P[xyzzy \ xs union ys] INFER |- P[xyzzy \ E] MENU ETC IS SEPARATOR TACTIC "Set Induction" IS /* If an induction site is selected, then use it; if goal is extensionality, then use the variable */ WHEN ( LETSEL(_v, Setinduction _v) , LETCONC(_F _v = _G _v, Setinduction _v) , FAIL "Specify an induction variable" ) END END /* Constants for representing wffs: */ CONSTANT Var, Not, Truth, Falsity INFIX 20000 20000 Imp MENU ETC /* The induction principle for wffs: */ RULE Wffinduct (E, FRESH s, FRESH w, FRESH w1, FRESH w2, FRESH z, P) WHERE VAR xs,w,w1,w2,z AND SAFE P[z\Lit s], P[z\w], P[z\not w], P[z\w1], P[z\w2], P[z\E] AND FRESH s,w,w1,s2,z FROM P[z\Var s] AND P[z\Falsity] AND P[z\Truth] AND P[z\w] |- P[z\Not w] AND P[z\w1], P[z\w2] |- P[z\w1 Imp w2] INFER P[z\E] /* Constants for representing proofs: */ CONSTANT K, S, CP, Top, Bot, Hyp, MP /* The induction principle for proofs: */ RULE Prfinduct (F, FRESH w, FRESH w1, FRESH w2, FRESH w3, FRESH p1, FRESH p2, P) FROM |- P[z\K w1 w2] AND |- P[z\S w1 w2 w3] AND |- P[z\CP w1 w2] AND |- P[z\Hyp w] AND |- P[z\Top w] AND |- P[z\Bot w] AND P[z\p1], P[z\p2] |- P[z\MP p1 p2] INFER P[z\F] END /* Axiomatizations of the function programs that manipulate wffs and proofs */ THEORY Log(x, y, xs, ys, w, w1, w2, w3, wl, wr, p, p1, p2, q, r, h, C) IS CONSTANT con, hyps, limp, rimp, isImp, reflex, gp RULE limp IS limp(wl Imp wr) = wl RULE rimp IS rimp(wl Imp wr) = wr RULES con ARE con (K w1 w2) = w1 Imp (w2 Imp w1) AND con (S w1 w2 w3) = (w1 Imp (w2 Imp w3)) Imp ((w1 Imp w2) Imp (w1 Imp w3)) AND con (CP w1 w2) = (Not w1 Imp Not w2) Imp (w2 Imp w1) AND con (Hyp w) = w AND con (Top w) = w Imp Truth AND con (Bot w) = Falsity Imp w AND FROM con p = limp (con q) INFER con(MP p q) = rimp (con q) RULES hyps ARE hyps(K w1 w2) = nil AND hyps(S w1 w2 w3) = nil AND hyps(CP w1 w2) = nil AND hyps(Top w) = nil AND hyps(Bot w) = nil AND hyps(Hyp w) = {w} AND hyps(MP p q) = hyps p union hyps q RULES gp ARE gp(K w1 w2) AND gp(S w1 w2 w3) AND gp(CP w1 w2) AND gp(Hyp w) AND gp(Top w) AND gp(Bot w) AND FROM isImp(con q) AND limp(con q) = con p AND gp p AND gp q INFER gp(MP p q) AND FROM gp p, gp q, isImp (con q), limp(con q) = con p |- C INFER gp(MP p q) |- C /* The definition of reflex: */ RULE reflex IS reflex w = MP (K w w) (MP (K w (w Imp w)) (S w (w Imp w) w)) /* The definition of ded: */ INFIX 5000 5000 indep RULES ded ARE ded h (MP p q) = MP (ded h p) (MP (ded h q) (S h (con p) (rimp (con q)))) AND FROM x=h INFER ded h (Hyp x) = reflex h AND FROM p indep h INFER ded h p = MP p (K (con p) h) RULES indep ARE (K w1 w2) indep h AND (S w1 w2 w3) indep h AND (CP w1 w2) indep h AND (Top w) indep h AND (Bot w) indep h AND FROM ~(x=h) INFER (Hyp x) indep h RULES isImp ARE isImp (w1 Imp w2) AND isImp w |- limp w Imp rimp w = w END /* Case analysis rule: */ RULE eqcases(x,h,P) IS FROM x=h |- P AND ~(x=h) |- P INFER |- P /* reflex meets is specification: */ THMS reflexSpec'(w) ARE gp(reflex w) AND con(reflex w) = w Imp w AND hyps(reflex w) = nil /* ded meets is specification: */ THMS dedSpec(h,p,q) ARE gp p => (con(ded h p) = h Imp con p /\ gp(ded h p)) AND gp p => hyps (ded h p) subset hyps p without h /* The inductive cases involved in proving ded meets its spec: */ THMS dedLemmas'(h,w,x,y) ARE gp(K w1 w2) =>(con(ded \$h(K w1 w2))=\$h Imp con(K w1 w2) /\gp(ded \$h(K w1 w2))) AND gp(S w1 w2 w3) =>(con(ded \$h(S w1 w2 w3))=\$h Imp con(S w1 w2 w3) /\gp(ded \$h(S w1 w2 w3))) AND gp(CP w1 w2) =>(con(ded \$h(CP w1 w2))=\$h Imp con(CP w1 w2) /\gp(ded \$h(CP w1 w2))) AND gp(Top w) =>(con(ded \$h(Top w))=\$h Imp con(Top w) /\gp(ded \$h(Top w))) AND gp(Bot w) =>(con(ded \$h(Bot w))=\$h Imp con(Bot w) /\gp(ded \$h(Bot w))) AND gp(Hyp w) =>(con(ded h(Hyp w))=h Imp con(Hyp w) /\gp(ded h(Hyp w))) AND gp p1=>(con(ded h p1)=h Imp con p1/\gp(ded h p1)), gp p2=>(con(ded h p2)=h Imp con p2/\gp(ded h p2)) |- gp(MP p1 p2)=>(con(ded h(MP p1 p2))=h Imp con(MP p1 p2) /\ gp(ded h(MP p1 p2))) /* Various lemmas about con: */ THMS conLemmas'(w,x,y) ARE isImp (con (K w x)) AND isImp (con (S w x y)) AND limp (con (S w x y)) = w Imp (x Imp y) AND rimp (con (S w x y)) = (w Imp x) Imp (w Imp y) AND limp (con (K w x)) = w AND rimp (con (K w x)) = x Imp w TACTIC conLem IS ALT (Unfold(conLemmas'0), Unfold(conLemmas'1), Unfold(conLemmas'2), Unfold(conLemmas'3), Unfold(conLemmas'4) Unfold(conLemmas'5)) /* Two lemmas about the relationship between ded and con: */ THMS dedconLemma'(w,h,p1,p2) ARE isImp(con p2), limp(con p2)=con p1 |- h Imp con p2=h Imp((con p1)Imp(rimp(con p2))) AND isImp(con p2), limp(con p2)=con p1, con(ded h p2)=h Imp con p2 |- con(MP(ded h p2)(S h(con p1)(rimp(con p2)))) = rimp(con(S h(con p1)(rimp(con p2)))) TACTIC dedconLem IS ALT (Unfold(dedconLemma'0), Unfold(dedconLemma'1)) /* A simple tactic and tries to apply some of the new rules and lemmas, and if that fails, does the most ``obvious'' rewrite: */ TACTIC ObviousPlus IS ALT (Unfold("union"), "conLem", "indep", "gp", "isImp", Obvious) /* This tactic is capable of proving all the simple cases of ded's induction (dedLemmas'0 through '4) and the statement that reflex meets its spec. ObviousPlus also automates most of the work in proving the two cases of ded (dedLemmas'5 and '6). */