(* theory of Boolean algebra and the cylindrical algebra of Tarski *) (* Boolean algebra part *) declareinfix "+"; declareinfix "*"; axiom "COMM1" "?x+?y" "?y+?x"; axiom "COMM2" "?x*?y" "?y*?x"; axiom "DIST1" "?x+?y*?z" "(?x+?y)*?x+?z"; axiom "DIST2" "?x*?y+?z" "(?x*?y)+?x*?z"; s "(?y*?z)+?x"; ri "COMM1"; ri "DIST1"; ex(); left(); ri "COMM1"; ex(); up(); right(); ri "COMM1"; ex(); up(); p "COMMDIST1"; s "(?y+?z)*?x"; ri "COMM2"; ri "DIST2"; ex(); left(); ri "COMM2"; ex(); up(); right(); ri "COMM2"; ex(); up(); p "COMMDIST2"; axiom "ID1" "0+?x" "?x"; axiom "ID2" "1*?x" "?x"; s "?x+0"; ri "COMM1"; ri "ID1"; ex(); p "COMMID1"; s "?x*1"; ri "COMM2"; ri "ID2"; ex(); p "COMMID2"; declareunary "-"; axiom "CANCEL1" "?x + -?x" "1"; axiom "CANCEL2" "?x* -?x" "0"; (* proving usual theorems in this system is something of an exercise *) (* idempotent laws *) s "?x"; rri "ID2"; ex(); left(); initializecounter(); rri "CANCEL1"; ex(); assign "?x_1" "?x"; top(); ri "COMM2"; ri "DIST2"; ex(); right(); ri "CANCEL2"; ex(); top(); ri "COMM1"; ri "ID1"; ex(); wb(); p "IDEM2"; s "?x"; rri "ID1"; ex(); left(); initializecounter(); rri "CANCEL2"; ex(); assign "?x_1" "?x"; top(); ri "COMM1"; ri "DIST1"; ex(); right(); ri "CANCEL1"; ex(); top(); ri "COMM2"; ri "ID2"; ex(); wb(); p "IDEM1"; (* absorption laws *) s "0*?x"; rri "ID1"; ex(); left(); initializecounter(); rri "CANCEL2"; ex(); assign "?x_1" "?x"; top(); ri "COMMDIST1"; ex(); left(); ri "DIST1"; ex(); right(); ri "IDEM1"; rri "COMMID1"; ex(); up(); ri "IDEM2"; ex(); up(); right(); ri "DIST1"; ex(); right(); ri "COMM1"; ri "CANCEL1"; ex(); up(); ri "COMMID2"; ex(); top(); rri "COMMDIST1"; ex(); left(); ri "CANCEL2"; ex(); up(); ri "ID1"; ex(); p "ABSORB1"; s "1+?x"; rri "ID2"; ex(); left(); initializecounter(); rri "CANCEL1"; ex(); assign "?x_1" "?x"; top(); ri "COMMDIST2"; ex(); left(); ri "DIST2"; ex(); right(); ri "IDEM2"; rri "COMMID2"; ex(); up(); ri "IDEM1"; ex(); up(); right(); ri "DIST2"; ex(); right(); ri "COMM2"; ri "CANCEL2"; ex(); up(); ri "COMMID1"; ex(); top(); rri "COMMDIST2"; ex(); left(); ri "CANCEL1"; ex(); up(); ri "ID2"; ex(); p "ABSORB2"; (* associative laws *) s "(?x+?y)+?z"; rri "ID2"; ex(); left(); initializecounter(); rri "CANCEL1"; ex(); assign "?x_1" "?y"; top(); ri "COMMDIST2"; ex(); left(); ri "DIST2"; ex(); left(); ri "DIST2"; ex(); right(); ri "IDEM2"; rri "COMMID2"; ex(); up(); rri "DIST2";ex(); up(); rri "DIST2";ex(); right(); left(); ri "COMM1"; ri "ABSORB2"; ex(); up(); ri "ABSORB2"; ex(); initializecounter(); rri "ABSORB2"; ex(); assign "?x_1" "?x"; ri "COMM1"; ex(); right(); initializecounter(); rri "ABSORB2"; ex(); assign "?x_1" "?z"; up();up(); ri "DIST2"; ex(); right(); ri "DIST2"; ex(); left(); ri "COMMID2"; rri "IDEM2"; ex(); up(); rri "DIST2"; ex(); up(); rri "DIST2"; ex(); up();right(); ri "DIST2"; ex(); left(); ri "DIST2"; ex(); right(); ri "COMM2"; ri "CANCEL2"; ex(); up(); ri "COMMID1"; ex(); up();right(); rri "ID1"; ex(); left(); initializecounter(); rri "CANCEL2"; ex(); ri "COMM2"; ex(); assign "?x_1" "?y"; up(); rri "DIST2"; ex(); up(); rri "DIST2"; ex(); up(); rri "COMMDIST2"; ex(); left(); ri "CANCEL1"; ex(); up(); ri "ID2"; ex(); p "ASSOC1"; s "(?x*?y)*?z"; rri "ID1"; ex(); left(); initializecounter(); rri "CANCEL2"; ex(); assign "?x_1" "?y"; top(); ri "COMMDIST1"; ex(); left(); ri "DIST1"; ex(); left(); ri "DIST1"; ex(); right(); ri "IDEM1"; rri "COMMID1"; ex(); up(); rri "DIST1";ex(); up(); rri "DIST1";ex(); right(); left(); ri "COMM2"; ri "ABSORB1"; ex(); up(); ri "ABSORB1"; ex(); initializecounter(); rri "ABSORB1"; ex(); assign "?x_1" "?x"; ri "COMM2"; ex(); right(); initializecounter(); rri "ABSORB1"; ex(); assign "?x_1" "?z"; up();up(); ri "DIST1"; ex(); right(); ri "DIST1"; ex(); left(); ri "COMMID1"; rri "IDEM1"; ex(); up(); rri "DIST1"; ex(); up(); rri "DIST1"; ex(); up();right(); ri "DIST1"; ex(); left(); ri "DIST1"; ex(); right(); ri "COMM1"; ri "CANCEL1"; ex(); up(); ri "COMMID2"; ex(); up();right(); rri "ID2"; ex(); left(); initializecounter(); rri "CANCEL1"; ex(); ri "COMM1"; ex(); assign "?x_1" "?y"; up(); rri "DIST1"; ex(); up(); rri "DIST1"; ex(); up(); rri "COMMDIST1"; ex(); left(); ri "CANCEL2"; ex(); up(); ri "ID1"; ex(); p "ASSOC2"; declareinfix "/"; (* use this for cylindrifications *) axiom "C1" "?q/0" "0"; axiom "C2" "?x+?q/?x" "?q/?x"; axiom "C3" "?q/?x*?q/?y" "(?q/?x)*?q/?y"; axiom "C4" "?q/?r/?x" "?r/?q/?x"; declareinfix "=="; axiom "C5" "?q==?q" "1"; axiom "C6" "?q/(?r==?q)*(?q==?s)" "(?q=?r)||1,(?q=?s)||1,?r==?s"; (* check that the unwanted alternatives really are 1 *) axiom "C7" "(?q/((?q==?r)*?x))*(?q/((?q==?r)* -?x))" "(?q=?r)||((?q/?x)*(?q/ -?x)),0"; s "(?x+?y)=0"; initializecounter(); ri "CASEINTRO";ex(); assign "?y_1" "?x=0"; right();left(); left();left(); ri "0|-|1"; ex(); up(); ri "ID1"; ex(); up();up();right(); ri "EQUATION"; ex(); right();left(); initializecounter(); rri "REFLEX"; ex(); assign "?a_1" "0"; left(); rri "0|-|2"; ex(); left(); rri "IDEM1"; ex(); up(); ri "ASSOC1"; ex(); right(); ri "0|-|2"; ex(); up(); ri "COMMID1"; ex(); up(); ri "EQUATION"; ri "1|-|1"; ex(); up();up(); rri "CASEINTRO"; ex(); p "LOGICLEMMA1"; s "(?x*?y)=1"; initializecounter(); ri "CASEINTRO";ex(); assign "?y_1" "?x=1"; right();left(); left();left(); ri "0|-|1"; ex(); up(); ri "ID2"; ex(); up();up();right(); ri "EQUATION"; ex(); right();left(); initializecounter(); rri "REFLEX"; ex(); assign "?a_1" "1"; left(); rri "0|-|2"; ex(); left(); rri "IDEM2"; ex(); up(); ri "ASSOC2"; ex(); right(); ri "0|-|2"; ex(); up(); ri "COMMID2"; ex(); up(); ri "EQUATION"; ri "1|-|1"; ex(); up();up(); rri "CASEINTRO"; ex(); p "LOGICLEMMA2"; defineinfix "LESSTHAN" "?x==?y" "?y=