(* intuitionistic logic, as per Gore, TR-ARP-6-95 and Dual Intuitionistic Logic Revisited TABLEAUX00: LNAI 1847:252-267, 2000 uses following structural connectives: o on right in paper is > here o on left in paper is ; here (ignore solid circle, for dual intuitionistic logic, in paper) display equivalence rules in paper are (sect 3.1) scAg "$X, $Y |- $Z == $Y |- $X > $Z" comA "$X, $Y |- $Z ==> $Y, $X |- $Z" structural rules in paper are (sect 3.2) wkrA "$X |- $Z ==> $X, $Y |- $Z" wklA "$X |- $Z ==> $Y, $X |- $Z" ctrA "$X, $X |- $Z ==> $X |- $Z" aA "$X, ($Y, $Z) |- $W == ($X, $Y); $Z |- $W" ila "$I, $X |- $Y == $X |- $Y" ils "$X |- $I, $Y == $X |- $Y" EfqI "$X |- $I ==> $X |- $Y" (and must identify $I and $phi) logical rules in paper are (sect 3.3) tA "$I |- $X ==> T |- $X" tS "$I |- T" fA "F |- $I" fS "$X |- $I ==> $X |- F" andal "A |- $X ==> A & B |- $X" andar "B |- $X ==> A & B |- $X" ands "[| $Z |- A, $Z |- B |] ==> $Z |- A & B" ora "[| A |- $Z ; B |- $Z |] ==> A v B |- $Z" orsl "$X |- A ==> $X |- A v B" orsr "$X |- B ==> $X |- A v B" (* derived intensional rules for conjunction *) anda_int "A, B |- $X ==> A & B |- $X" ands_int "[| $Y |- A, $X |- B |] ==> $Y, $X |- A & B" rarrA "[| $X |- A ; B |- $Y |] ==> A -> B |- $X > $Y" rarrS "$X |- A > B ==> $X |- A -> B" (* Identity rule for formulae *) idf "A |- A" (* Cut rule *) cut "[| $X |- A ; A |- $Y |] ==> $X |- $Y" *) (* proof of 10 intuitionistic logic axioms, as given by Belnap, Display Logic, pp 405-6 *) (* still need to check that these use only the rules above *) fun tacss str _ = [ (glob_tac (tfpr pr_intr) 1), ALLGOALS (disp_tac str), ALLGOALS (keep1_tac), ALLGOALS (rtac idf)] ; val I1 = prove_goal thy "$I |- A -> (B -> A)" (tacss "-rr") ; val I3 = prove_goal thy "$I |- (A & B) -> A" (tacss "-r") ; val I4 = prove_goal thy "$I |- (A & B) -> B" (tacss "-r") ; val I5 = prove_goal thy "$I |- A -> (B -> (A & B))" (tacss "-rr") val I6 = prove_goal thy "$I |- A -> (A v B)" (tacss "-r") ; val I7 = prove_goal thy "$I |- B -> (A v B)" (tacss "-r") ; (* mpl - for modus ponens on the left, "B |- $Z ==> A, A -> B |- $Z" *) val mpl = idf RS (fdisp "-r" rarrA) ; val mpl' = mpl RS comA ; val pr_mp = make_prt ([mpl, mpl'], []) ; (* dual to mpl *) val rmpl = idf RSN (2, fdisp "|l" butnotS) ; val cont = prove_goal thy "A & (A -> F) |- $I" (fn _ => [ (glob_tac (tfpr pr_intr) 1), (rtac cut 1), (rtac fA 2), (rtac (idf RS mpl) 1)]) ; val exm = prove_goal thy "$I |- (T -< A) v A" (fn _ => [ (glob_tac (tfpr pr_intr) 1), (rtac cut 1), (rtac tS 1), (rtac (idf RS rmpl) 1)]) ; (* double negations - replace B by F, T *) val nnI = prove_goal thy "A |- (A -> B) -> B" (fn _ => [ (glob_tac (tfpr pr_intr) 1), (disp_tac "-l" 1), (rtac (rarrA RS md1 revarrS) 1), (ALLGOALS (rtac idf))] ) ; val nnD = prove_goal thy "B -< (B -< A) |- A" (fn _ => [ (glob_tac (tfpr pr_intr) 1), (disp_tac "|r" 1), (rtac (butnotS RS md2 revarrA) 1), (ALLGOALS (rtac idf))] ) ; (* from Gore, TABLEAUX00, Fig 4 *) val not_not = prove_goal thy "A -> F |- T -< A" (fn _ => [ (rtac (md1 ila) 1), (d_b_tac "|l" (rtac (ora RS (exm RS cut))) 1), (rtac (idf RS wkrA) 1), (rtac mpl 1), (rtac (fA RS EfqI) 1)]) ; (* mixed double negations *) val mnD = prove_goal thy "(T -< A) -> F |- A" (fn _ => [ (rtac (md1 ils) 1), (d_b_tac "-l" (rtac (cont RSN (2, cut)) THEN' rtac ands) 1), (rtac wkrS 2), (rtac idf 2), (rtac ors_int_inv 1), (rtac VerI 1), (rtac exm 1)]) ; val mnI = prove_goal thy "A |- T -< (A -> F)" (fn _ => [ (rtac (md1 ira) 1), (d_b_tac "|r" (rtac (exm RSN (1, cut)) THEN' rtac ora) 1), (rtac wklA 1), (rtac idf 1), (rtac anda_int_inv 1), (rtac EfqI 1), (rtac cont 1)]) ; val I2 = prove_goal thy "$I |- (A -> B) -> (A -> B -> C) -> (A -> C)" (fn _ => [ (glob_tac (tfpr pr_intr) 1), (disp_tac "-rrr" 1), (d_b_tac "|l" (rtac ctrA) 1), (rtac (md2 aA) 1), (d_b_tac "|l" (rtac (md1 aA)) 1), (glob_tac (tfpr pr_mp) 1), (glob_tac (tfpr pr_id) 1), (d_b_tac "|l" (rtac comA) 1), (rtac (md1 aA) 1), (bup_tac (tfpr pr_mp) 1), rtac idf 1]) ; val I9 = prove_goalw thy [not_def] "$I |- (A -> B) -> (A -> ~ B) -> ~ A" (fn _ => [ (rtac I2 1) ]) ; val I10 = prove_goalw thy [not_def] "$I |- A -> (~ A -> B)" (fn _ => [ (glob_tac (tfpr pr_intr) 1), (disp_tac "-rr" 1), (bup_tac (tfpr (pr_appl [pr_id, pr_mp, pr_intr])) 1) ]) ; val mp = prove_goal thy "[| $I |- A ; $I |- A -> B |] ==> $I |- B" (fn [pa, pab] => [ (rtac (pa RS cut) 1), (rtac (md1 ira) 1), (disp_tac "|r" 1), (rtac (pab RS cut) 1), (rtac rarrA 1), (ALLGOALS (rtac idf))]) ;