(* 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" "(?x+?y)=?y";

s "?x=?x*?y";
initializecounter();
ri "CASEINTRO"; ex();
assign "?y_1" "(?x+?y)=?y";
right();left();
right();right();
rri "0|-|1"; ex();
up();
ri "DIST2"; ex();
left();
ri "IDEM2"; rri "COMMID2"; ex();
up();
rri "DIST2"; ex();
right();
ri "ABSORB2"; ex();
up();
ri "COMMID2"; ex();
up();
ri "REFLEX"; ex();
up();right();
ri "EQUATION"; ex();
right();left();
initializecounter();
rri "REFLEX"; ex();
assign "?a_1" "?x+?y";
right();left();
ri "0|-|2"; ex();
up();right();
rri "ID2"; ex();
up();
rri "COMMDIST2"; ex();
left();
ri "COMM1"; ri "ABSORB2"; ex();
up();
ri "ID2"; ex();
up();
ri "EQUATION"; ri "1|-|1"; ex();
up();up();
rri "CASEINTRO"; ex();
top();
rri "EQUATION"; ex();
rri "LESSTHAN"; ex();
p "DUALDEF";

s "?x=?x*?y";
initializecounter();
ri "CASEINTRO"; ex();
assign "?y_1" "(?x* -?y)=0";
right();left();
left();
rri "COMMID2"; ex();
right();
initializecounter();
rri "CANCEL1"; ex();
assign "?x_1" "?y";
up();
ri "DIST2"; ex();
right();
ri "0|-|1"; ex();
up();
ri "COMMID1"; ex();
up();
ri "REFLEX"; ex();
up();right();
ri "DUALDEF"; ri "LESSTHAN"; ex();
ri "EQUATION"; ex();
right();left();
initializecounter();
rri "REFLEX"; ex();
assign "?a_1" "?x* -?y";
right();
rri "COMMID1"; ex();
right();
initializecounter();
rri "CANCEL2"; ex();
assign "?x_1" "?y";
up();
rri "COMMDIST2"; ex();
left();
ri "0|-|2"; ex();
up();
ri "CANCEL2"; ex();
up();
ri "EQUATION"; ri "1|-|1"; ex();
up();up();
rri "CASEINTRO"; ex();
top();
rri "EQUATION"; ex();
wb();
ri "DUALDEF"; ex();
p "SUBDEF";


defineinfix "GREATERTHAN" "?x>=?y" "?y=<?x";

start "?x=?y";
initializecounter();
ri "CASEINTRO"; ex();
assign "?y_1" "?x=<?y";
left();
ri "LESSTHAN"; ex();
top();
right();right();
ri "EQUATION"; ex();
right();left();
initializecounter();
rri "REFLEX"; ex();
assign "?a_1" "?x";
left();
rri "IDEM1"; ex();
right();
ri "0|-|2"; ex();
up();up();right();
ri "0|-|2"; ex();
up();
ri "EQUATION"; ri "1|-|1"; ex();
up();up();
rri "CASEINTRO"; ex();
up();left();
initializecounter();
ri "CASEINTRO"; ex();
assign "?y_1" "?y=<?x";
left();
ri "LESSTHAN"; ex();
up();
right();right();
ri "EQUATION"; ex();
right();left();
initializecounter();
rri "REFLEX"; ex();
assign "?a_1" "?x";
left();
rri "IDEM1"; ex();
left();
ri "0|-|3"; ex();
up();
up();
ri "EQUATION"; ri "1|-|2"; ex();
up();up();
rri "CASEINTRO"; ex();
up();left();
left();
rri "0|-|2"; ex();
up();right();
rri "0|-|1"; ri "COMM1"; ex();
up(); 
ri "REFLEX"; ex();
up();up();
rri "EQUATION"; ex();
rri "LESSTHAN"; ex();
up();up();left();
rri "LESSTHAN"; ex();
p "TWOWAYS";

s "?x = - - ?x";
ri "TWOWAYS"; ex();
left();
rri "DUALDEF"; ex();
right();
rri "ID1"; ex();
left();
initializecounter();
rri "CANCEL2"; ex();
assign "?x_1" "?x";
up();
rri "DIST2"; ex();
right();
ri "CANCEL1"; ex();
up();
ri "COMMID2"; ex();
up(); ri "REFLEX"; ex();
up(); ex();
rri "SUBDEF"; ex();
left();
ri "COMM2"; ex();
ri "CANCEL2"; ex();
up(); 
ri "REFLEX"; ex();
p "DUBNEGa";

s "- -?x";
initializecounter();
ri "CASEINTRO"; ex();
assign "?y_1" "?x = - - ?x";
right();left();
rri "0|-|1"; ex();
top();left();
ri "DUBNEGa"; ex();
up(); ex();
p "DUBNEG";

(* theorems from Tarski *)

(* starting on p. 175 of the book *)

s "(?q/?x)=0";
initializecounter();
ri "CASEINTRO"; ex();
assign "?y_1" "?x=0";
right();left();
left();right();
ri "0|-|1"; ex();
up();up();left();
ri "C1"; ex();
up();
ri "REFLEX"; ex();
up();right();
ri "EQUATION"; ex();
right();left();
initializecounter();
rri "REFLEX"; ex();
assign "?a_1" "?q/?x";
left();
rri "C2"; ex();
right();
ri "0|-|2"; ex();
up();
ri "COMM1"; ri "ID1"; ex();
up();right();
ri "0|-|2"; ex();
up();
ri "EQUATION"; ri "1|-|1"; ex();
up();up();
rri "CASEINTRO"; ex();
top();
rri "EQUATION"; ex();
p "T1";

s "?q/1";
rri "C2"; ex();
ri "ABSORB2"; ex();
p "T2";

s "?q/?q/?x";
right();
rri "ID2"; ex();
top();
ri "C3"; ex();
left(); ri "T2"; ex();
top();
ri "ID2"; ex();
p "T3";

s "?x=?q/?x";
initializecounter();
ri "CASEINTRO"; ex();
assign "?y_1" "[?x=?1/?x]=[false]";

(* complete the proof of the metastatement which constitutes T4 *)

s "(?x*?q/?y)=0";
initializecounter();
rri "T1"; ex();
assign "?q_1" "?q";
left();
ri "C3"; ri "COMM2"; rri "C3"; ex();
up();
ri "T1"; ex();
p "T5";

(* the form of this argument is very challenging in Mark2! *)

s "true";
initializecounter();
rri "REFLEX"; ex();
assign "?a_1" "0";
left();
initializecounter();
rri "CANCEL2"; ri "COMM2"; ex();
assign "?x_1" "?q/?x+?y";
top();
ri "T5"; ex();
left();
ri "COMMDIST2"; ex();
up();
ri "LOGICLEMMA1"; ex();
left();
ri "T5"; ex();
up(); right();left();
ri "T5"; ex();
p "T6i";

initializecounter();
ae "T6i";
assign "?q_1+?x_1+?y_1" "?q+?x+?y";
initializecounter();
ri "CASEINTRO"; ex();
assign "?y_1" "((- ?q / ?x + ?y) * ?q / ?x) = 0";
right();right();
ri "1|-|1"; ex();
up();left();
rri "T6i"; ex();
top();
rri "EQUATION"; ex();
p "T6ia";

(* with the use of TWOWAYS I should be able to complete the argument 
as in Tarski.  The distinction between the logic in the theory and the
meta-logic is quite clear here--and both are being handled!  *)

s "(?q/?x+?y) = (?q/?x)+?q/?y";
ri "TWOWAYS"; ex();
left();
rri "SUBDEF"; ex();
left();
ri "COMM2"; ex();
up();
ri "T5"; ex();
left();
ri "COMMDIST2"; ex();
up();
ri "LOGICLEMMA1"; ex();
left();
ri "T5"; ex();
left();
ri "COMM2"; ex();
up();
ri "SUBDEF"; ex();
ri "LESSTHAN"; ex();
left();
rri "ASSOC1";ex();
left();
ri "IDEM1"; ex();
up();up();
ri "REFLEX"; ex();
up(); ex();
ri "T5"; ex();
left();
ri "COMM2"; ex();
up();
ri "SUBDEF"; ri "LESSTHAN"; ex();
left();
ri "COMM1"; ri "ASSOC1"; ex();
right();
ri "IDEM1"; ex();
up();up();
ri "REFLEX"; ex();
up(); ex();
rri "SUBDEF"; ex();
left();
ri "COMMDIST2"; ex();
left(); ri "COMM2"; ex();
up(); right(); ri "COMM2"; ex();
up();up();
ri "LOGICLEMMA1"; ex();
left();
rri "T6ia"; ex();
up(); ex();
downtoleft "?x+?y";
ri "COMM1"; ex();
top();
rri "T6ia";ex();
p "CYLDISTa";





quit();