Print["AXIOMS.M         Revised 1998 September 21"]
(*
   Quaife's axioms and definitions, modified to remove all Skolem
   functions.  The Axiom of Choice assures the existence of a
   member of any nonempty set, which is crucial for removing the
   Skolem function in axa1b.
*)

PrintDate[]

startdate = Date[]; kount = count

Print[""]; Print["Quaife's Axioms, Group A"]; Print[""];

example[axa1a,"implies[subclass[x,y],implies[member[u,x],member[u,y]]]",
"definition of subclass"]

example[axa1b,"implies[equal[0,intersection[x,complement[y]]],
subclass[x,y]]","definition of subclass"]

example[axa2,"subclass[x,V]",
"all members of a class x are members of V"]

example[axa3a,"subclass[x,x]",
"converse of coextension axiom"]

example[axa3b,"implies[and[subclass[x,y],subclass[y,x]],equal[x,y]]",
"extensionality axiom"]

example[axa4a,"member[pairset[x,y],V]",
"axiom of pairing"]

example[axa4b,"implies[member[u,pairset[x,y]],or[equal[u,x],equal[u,y]]]",
"definition of pairset"]

example[axa4c,"implies[member[x,V],member[x,pairset[x,y]]]",
"definition of pairset"]

example[axa4d,"implies[member[y,V],member[y,pairset[x,y]]]",
"definition of pairset"]

Print[""]; Print["Definition Group A"]; Print[""];

example[dfa1,"equal[singleton[x],pairset[x,x]]",
"definition of singleton"]

(*  Removed 98 January 24 *)
example[dfa2,"equal[pair[x,y],
pairset[singleton[x],pairset[x,singleton[y]]]]",
"Quaife's modification of Kuratowski's definition"]

Print[""]; Print["Quaife's Axiom Group B"]; Print[""];

example[axb1a,"subclass[E,cart[V,V]]","elementhood relation"]

example[axb1b,"implies[member[pair[x,y],E],member[x,y]]",
"elementhood relation"]

example[axb1c,"implies[and[member[pair[x,y],cart[V,V]],
member[x,y]],member[pair[x,y],E]]","elementhood relation"]

example[axb2a,"implies[member[z,intersection[x,y]],member[z,x]]",
"binary intersection"]

example[axb2b,"implies[member[z,intersection[x,y]],member[z,y]]",
"binary intersection"]

example[axb2c,"implies[and[member[z,x],member[z,y]],
member[z,intersection[x,y]]]","binary intersection"]

example[axb3a,"implies[member[z,complement[x]],not[member[z,x]]]",
"complement"]

example[axb3b,"implies[and[member[z,V],not[member[z,x]]],
member[z,complement[x]]]","complement"]

example[axb4a,"implies[member[z,domain[x]],
not[equal[restrict[x,singleton[z],V],0]]]","domain"]

example[axb4b,"implies[and[member[z,V],
not[equal[restrict[x,singleton[z],V],0]]],member[z,domain[x]]]","domain"]

Print[""]; Print["Quaife's Axiom B-5'a"]; Print[""];

example[cart1,"implies[member[pair[u,v],cart[x,y]],member[u,x]]",
"axiom of cartesian product"]

example[cart2,"implies[member[pair[u,v],cart[x,y]],member[v,y]]",
"axiom of cartesian product"]

example[cart3,"implies[and[member[u,x],member[v,y]],
member[pair[u,v],cart[x,y]]]","axiom of cartesian product"]

Print[""]; Print["Definition Group B"]; Print[""];

example[dfb1,"equal[union[x,y],
complement[intersection[complement[x],complement[y]]]]",
"definition of union"]

example[dfb2,"equal[symmdiff[x,y],
intersection[union[x,y],complement[intersection[x,y]]]]",
"definition of symmetric difference"]

example[dfb3,"equal[restrict[z,x,y],intersection[z,cart[x,y]]]",
"restriction"]

example[dfb4,"equal[inverse[y],domain[flip[cart[y,V]]]]","inverse"]

example[dfb5,"equal[range[z],domain[inverse[z]]]","range"]

example[dfb6,"equal[image[z,x],range[restrict[z,x,V]]]","image"]

example[axb7a,"subclass[rotate[x],cart[cart[V,V],V]]","rotate axiom"]

example[axb7b,"implies[member[pair[pair[u,v],w],rotate[x]],
member[pair[pair[v,w],u],x]]","rotate definition"]

example[axb7c,"implies[and[member[pair[pair[u,v],w],x],
member[pair[pair[u,v],w],cart[cart[V,V],V]]],
member[pair[pair[w,u],v],rotate[x]]]","rotate"]

(* revised 9/17/96 *)
example[axb8a,"subclass[flip[x],cart[cart[V,V],V]]","flip"]

example[axb8b,"implies[member[pair[pair[v,u],w],flip[x]],
member[pair[pair[u,v],w],x]]","flip"]

example[axb8c,"implies[and[member[pair[pair[u,v],w],x],
member[pair[pair[u,v],w],cart[cart[V,V],V]]],
member[pair[pair[v,u],w],flip[x]]]","flip"]

Print[""]; Print["Definition Group C"]; Print[""];

example[dfc1,"equal[succ[x],union[x,singleton[x]]]",
"successor class"]

example[dfc2a,"subclass[SUCC,cart[V,V]]",
"SUCC = successor function"]

example[dfc2b,"implies[member[pair[x,y],SUCC],equal[y,succ[x]]]",
"SUCC = successor function"]

example[dfc2c,"implies[and[member[pair[x,y],cart[V,V]],equal[y,succ[x]]],
member[pair[x,y],SUCC]]","SUCC = successor function"]

example[dfc3a,"implies[INDUCTIVE[x],member[0,x]]","INDUCTIVE"]

example[dfc3b,"implies[INDUCTIVE[x],
subclass[image[SUCC,x],x]]","INDUCTIVE"]

example[dfc3b,"implies[and[member[0,x],subclass[image[SUCC,x],x]],
INDUCTIVE[x]]","INDUCTIVE"]

example[dfc4,"equal[domain[restrict[E,V,x]],U[x]]","sum class"]

example[dfc5,"equal[complement[image[E,complement[x]]],P[x]]",
"power class"]

example[dfc6a,"subclass[composite[x,y],cart[V,V]]",
"composition"]

example[dfc6b,"implies[member[pair[u,v],composite[x,y]],
member[v,image[x,image[y,singleton[u]]]]]","composition"]

example[dfc6c,"implies[member[pair[u,v],composite[x,y]],
member[v,image[x,image[y,singleton[u]]]]]","composition"]

example[dfc6d,"implies[and[member[pair[u,v],cart[V,V]],
member[v,image[x,image[y,singleton[u]]]]],
member[pair[u,v],composite[x,y]]]","composition"]

example[dfc7a,"implies[FUNCTION[z],subclass[z,cart[V,V]]]",
"function"]

Print[""]; Print["Axiom Group C"]; Print[""];

example[axc1b,"implies[INDUCTIVE[y],subclass[omega,y]]",
"axiom of infinity"]

example[axc1c,"member[omega,V]","axiom of infinity"]

example[axc2,"implies[member[x,V],member[U[x],V]]",
"axiom of sum class"]

example[axc3,"implies[member[x,V],member[P[x],V]]",
"axiom of power class"]

example[axc4,"implies[and[member[x,V],FUNCTION[z]],member[image[z,x],V]]",
"axiom of replacement"]

Print[""]; Print["Axiom Group D"]; Print[""];

example[axd1a,"implies[not[equal[x,0]],
not[equal[0,intersection[x,P[complement[x]]]]]]",
"axiom of regularity with Skolem function eliminated"]

Print[""]; Print["Axiom Group E"]; Print[""];

example[axe1,"FUNCTION[CHOICE]",
"axiom of universal choice"]

example[axe2,"subclass[CHOICE,inverse[E]]",
"axiom of universal choice"]

example[axe3,"equal[domain[CHOICE],complement[singleton[0]]]",
"axiom of universal choice"]

example[axe4,"implies[and[member[x,V],not[equal[x,0]]],
member[apply[CHOICE,x],x]]",
"Quaife's formulation for axe2 and axe3"]

Print[""]; Print["Total number of Axioms and Definitions: ", count - kount];

elapsedtime = Date[] - startdate

Print[""]; Print["Total Elapsed Time:  ", 
elapsedtime[[6]] + 60 (elapsedtime[[5]] + 
60 (elapsedtime[[4]] + 24 elapsedtime[[3]])),
" Seconds"]