In[1]:= << convert.m; << axioms.m CONVERT.M created 1998 September 21 at 10:30 a.m. It is now: 2001 Jan 23 at 8:21 AXIOMS.M Revised 1998 September 21 It is now: 2001 Jan 23 at 8:21 Quaife's Axioms, Group A In[axa1a]:= implies[subclass[x,y],implies[member[u,x],member[u,y]]] definition of subclass Out[axa1a]= equal[V, union[complement[image[V, > intersection[x, singleton[u]]]], > image[V, intersection[x, complement[y]]], > image[V, intersection[y, singleton[u]]]]] Execution time = 0 Seconds In[axa1b]:= implies[equal[0,intersection[x,complement[y]]], subclass[x,y]] definition of subclass Out[axa1b]= True Execution time = 0 Seconds In[axa2]:= subclass[x,V] all members of a class x are members of V Out[axa2]= True Execution time = 0 Seconds In[axa3a]:= subclass[x,x] converse of coextension axiom Out[axa3a]= True Execution time = 0 Seconds In[axa3b]:= implies[and[subclass[x,y],subclass[y,x]],equal[x,y]] extensionality axiom Out[axa3b]= True Execution time = 0 Seconds In[axa4a]:= member[pairset[x,y],V] axiom of pairing Out[axa4a]= equal[V, image[V, singleton[pairset[x, y]]]] Execution time = 0 Seconds In[axa4b]:= implies[member[u,pairset[x,y]],or[equal[u,x],equal[u,y]]] definition of pairset Out[axa4b]= equal[V, union[complement[image[V, > intersection[pairset[x, y], singleton[u]]]], > intersection[complement[image[V, intersection[u, complement[x]]]], > complement[image[V, intersection[x, complement[u]]]]], > intersection[complement[image[V, intersection[u, complement[y]]]], > complement[image[V, intersection[y, complement[u]]]]]]] Execution time = 0 Seconds In[axa4c]:= implies[member[x,V],member[x,pairset[x,y]]] definition of pairset Out[axa4c]= equal[V, union[complement[image[V, singleton[x]]], > image[V, intersection[pairset[x, y], singleton[x]]]]] Execution time = 0 Seconds In[axa4d]:= implies[member[y,V],member[y,pairset[x,y]]] definition of pairset Out[axa4d]= equal[V, union[complement[image[V, singleton[y]]], > image[V, intersection[pairset[x, y], singleton[y]]]]] Execution time = 0 Seconds Definition Group A In[dfa1]:= equal[singleton[x],pairset[x,x]] definition of singleton Out[dfa1]= equal[V, union[intersection[complement[pairset[x, x]], > complement[singleton[x]]], intersection[pairset[x, x], singleton[x]]]] Execution time = 0 Seconds In[dfa2]:= equal[pair[x,y], pairset[singleton[x],pairset[x,singleton[y]]]] Quaife's modification of Kuratowski's definition Out[dfa2]= equal[V, union[intersection[complement[pair[x, y]], > complement[pairset[singleton[x], pairset[x, singleton[y]]]]], > intersection[pair[x, y], pairset[singleton[x], > pairset[x, singleton[y]]]]]] Execution time = 0 Seconds Quaife's Axiom Group B In[axb1a]:= subclass[E,cart[V,V]] elementhood relation Out[axb1a]= equal[V, union[cart[V, V], complement[E]]] Execution time = 0 Seconds In[axb1b]:= implies[member[pair[x,y],E],member[x,y]] elementhood relation Out[axb1b]= equal[V, union[complement[image[V, > intersection[E, singleton[pair[x, y]]]]], > image[V, intersection[y, singleton[x]]]]] Execution time = 0 Seconds In[axb1c]:= implies[and[member[pair[x,y],cart[V,V]],\ > member[x,y]],member[pair[x,y],E]] elementhood relation Out[axb1c]= equal[V, union[complement[image[V, > intersection[y, singleton[x]]]], > complement[image[V, intersection[cart[V, V], singleton[pair[x, y]]]]], > image[V, intersection[E, singleton[pair[x, y]]]]]] Execution time = 0 Seconds In[axb2a]:= implies[member[z,intersection[x,y]],member[z,x]] binary intersection Out[axb2a]= True Execution time = 0 Seconds In[axb2b]:= implies[member[z,intersection[x,y]],member[z,y]] binary intersection Out[axb2b]= True Execution time = 0 Seconds In[axb2c]:= implies[and[member[z,x],member[z,y]], member[z,intersection[x,y]]] binary intersection Out[axb2c]= equal[V, union[complement[image[V, > intersection[x, singleton[z]]]], > complement[image[V, intersection[y, singleton[z]]]], > image[V, intersection[x, y, singleton[z]]]]] Execution time = 0 Seconds In[axb3a]:= implies[member[z,complement[x]],not[member[z,x]]] complement Out[axb3a]= equal[V, union[complement[image[V, > intersection[x, singleton[z]]]], > complement[image[V, intersection[complement[x], singleton[z]]]]]] Execution time = 0 Seconds In[axb3b]:= implies[and[member[z,V],not[member[z,x]]],\ > member[z,complement[x]]] complement Out[axb3b]= equal[V, union[complement[image[V, singleton[z]]], > image[V, intersection[x, singleton[z]]], > image[V, intersection[complement[x], singleton[z]]]]] Execution time = 0 Seconds In[axb4a]:= implies[member[z,domain[x]],\ > not[equal[restrict[x,singleton[z],V],0]]] domain Out[axb4a]= equal[V, union[complement[image[V, > intersection[domain[x], singleton[z]]]], > image[V, restrict[x, singleton[z], V]]]] Execution time = 0 Seconds In[axb4b]:= implies[and[member[z,V],\ > not[equal[restrict[x,singleton[z],V],0]]],member[z,domain[x]]] domain Out[axb4b]= equal[V, union[complement[image[V, > restrict[x, singleton[z], V]]], complement[image[V, singleton[z]]], > image[V, intersection[domain[x], singleton[z]]]]] Execution time = 0 Seconds Quaife's Axiom B-5'a In[cart1]:= implies[member[pair[u,v],cart[x,y]],member[u,x]] axiom of cartesian product Out[cart1]= equal[V, union[complement[image[V, > intersection[cart[x, y], singleton[pair[u, v]]]]], > image[V, intersection[x, singleton[u]]]]] Execution time = 0 Seconds In[cart2]:= implies[member[pair[u,v],cart[x,y]],member[v,y]] axiom of cartesian product Out[cart2]= equal[V, union[complement[image[V, > intersection[cart[x, y], singleton[pair[u, v]]]]], > image[V, intersection[y, singleton[v]]]]] Execution time = 0 Seconds In[cart3]:= implies[and[member[u,x],member[v,y]], member[pair[u,v],cart[x,y]]] axiom of cartesian product Out[cart3]= equal[V, union[complement[image[V, > intersection[x, singleton[u]]]], > complement[image[V, intersection[y, singleton[v]]]], > image[V, intersection[cart[x, y], singleton[pair[u, v]]]]]] Execution time = 0 Seconds Definition Group B In[dfb1]:= equal[union[x,y],\ > complement[intersection[complement[x],complement[y]]]] definition of union Out[dfb1]= True Execution time = 0 Seconds In[dfb2]:= equal[symmdiff[x,y],\ > intersection[union[x,y],complement[intersection[x,y]]]] definition of symmetric difference Out[dfb2]= equal[V, union[intersection[x, y, complement[symmdiff[x, y]]], > intersection[x, complement[y], symmdiff[x, y]], > intersection[y, complement[x], symmdiff[x, y]], > intersection[complement[x], complement[y], complement[symmdiff[x, y]]]]] Execution time = 0 Seconds In[dfb3]:= equal[restrict[z,x,y],intersection[z,cart[x,y]]] restriction Out[dfb3]= equal[V, union[intersection[complement[z], > complement[restrict[z, x, y]]], > intersection[complement[cart[x, y]], complement[restrict[z, x, y]]], > intersection[z, cart[x, y], restrict[z, x, y]]]] Execution time = 0 Seconds In[dfb4]:= equal[inverse[y],domain[flip[cart[y,V]]]] inverse Out[dfb4]= equal[V, union[intersection[complement[domain[flip[cart[y, V]]]], > complement[inverse[y]]], > intersection[domain[flip[cart[y, V]]], inverse[y]]]] Execution time = 0 Seconds In[dfb5]:= equal[range[z],domain[inverse[z]]] range Out[dfb5]= equal[V, union[intersection[complement[domain[inverse[z]]], > complement[range[z]]], intersection[domain[inverse[z]], range[z]]]] Execution time = 0 Seconds In[dfb6]:= equal[image[z,x],range[restrict[z,x,V]]] image Out[dfb6]= equal[V, union[intersection[complement[image[z, x]], > complement[range[restrict[z, x, V]]]], > intersection[image[z, x], range[restrict[z, x, V]]]]] Execution time = 0 Seconds In[axb7a]:= subclass[rotate[x],cart[cart[V,V],V]] rotate axiom Out[axb7a]= equal[V, union[cart[cart[V, V], V], complement[rotate[x]]]] Execution time = 0 Seconds In[axb7b]:= implies[member[pair[pair[u,v],w],rotate[x]],\ > member[pair[pair[v,w],u],x]] rotate definition Out[axb7b]= equal[V, union[complement[image[V, > intersection[rotate[x], singleton[pair[pair[u, v], w]]]]], > image[V, intersection[x, singleton[pair[pair[v, w], u]]]]]] Execution time = 0 Seconds In[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 Out[axb7c]= equal[V, union[complement[image[V, > intersection[x, singleton[pair[pair[u, v], w]]]]], > complement[image[V, intersection[cart[cart[V, V], V], > singleton[pair[pair[u, v], w]]]]], > image[V, intersection[rotate[x], singleton[pair[pair[w, u], v]]]]]] Execution time = 0 Seconds In[axb8a]:= subclass[flip[x],cart[cart[V,V],V]] flip Out[axb8a]= equal[V, union[cart[cart[V, V], V], complement[flip[x]]]] Execution time = 0 Seconds In[axb8b]:= implies[member[pair[pair[v,u],w],flip[x]],\ > member[pair[pair[u,v],w],x]] flip Out[axb8b]= equal[V, union[complement[image[V, > intersection[flip[x], singleton[pair[pair[v, u], w]]]]], > image[V, intersection[x, singleton[pair[pair[u, v], w]]]]]] Execution time = 0 Seconds In[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 Out[axb8c]= equal[V, union[complement[image[V, > intersection[x, singleton[pair[pair[u, v], w]]]]], > complement[image[V, intersection[cart[cart[V, V], V], > singleton[pair[pair[u, v], w]]]]], > image[V, intersection[flip[x], singleton[pair[pair[v, u], w]]]]]] Execution time = 0 Seconds Definition Group C In[dfc1]:= equal[succ[x],union[x,singleton[x]]] successor class Out[dfc1]= equal[V, union[intersection[x, succ[x]], > intersection[singleton[x], succ[x]], > intersection[complement[x], complement[singleton[x]], > complement[succ[x]]]]] Execution time = 0 Seconds In[dfc2a]:= subclass[SUCC,cart[V,V]] SUCC = successor function Out[dfc2a]= equal[V, union[cart[V, V], complement[SUCC]]] Execution time = 0 Seconds In[dfc2b]:= implies[member[pair[x,y],SUCC],equal[y,succ[x]]] SUCC = successor function Out[dfc2b]= equal[V, union[complement[image[V, > intersection[SUCC, singleton[pair[x, y]]]]], > intersection[complement[image[V, > intersection[y, complement[succ[x]]]]], > complement[image[V, intersection[complement[y], succ[x]]]]]]] Execution time = 0 Seconds In[dfc2c]:= implies[and[member[pair[x,y],cart[V,V]],equal[y,succ[x]]],\ > member[pair[x,y],SUCC]] SUCC = successor function Out[dfc2c]= equal[V, union[complement[image[V, > intersection[cart[V, V], singleton[pair[x, y]]]]], > image[V, intersection[SUCC, singleton[pair[x, y]]]], > image[V, intersection[y, complement[succ[x]]]], > image[V, intersection[complement[y], succ[x]]]]] Execution time = 0 Seconds In[dfc3a]:= implies[INDUCTIVE[x],member[0,x]] INDUCTIVE Out[dfc3a]= True Execution time = 0 Seconds In[dfc3b]:= implies[INDUCTIVE[x], subclass[image[SUCC,x],x]] INDUCTIVE Out[dfc3b]= True Execution time = 0 Seconds In[dfc3b]:= implies[and[member[0,x],subclass[image[SUCC,x],x]], INDUCTIVE[x]] INDUCTIVE Out[dfc3b]= True Execution time = 0 Seconds In[dfc4]:= equal[domain[restrict[E,V,x]],U[x]] sum class Out[dfc4]= equal[V, union[intersection[complement[domain[restrict[E, V, x]]], > complement[U[x]]], intersection[domain[restrict[E, V, x]], U[x]]]] Execution time = 0 Seconds In[dfc5]:= equal[complement[image[E,complement[x]]],P[x]] power class Out[dfc5]= equal[V, union[intersection[complement[image[E, complement[x]]], > P[x]], intersection[complement[P[x]], image[E, complement[x]]]]] Execution time = 0 Seconds In[dfc6a]:= subclass[composite[x,y],cart[V,V]] composition Out[dfc6a]= equal[V, union[cart[V, V], complement[composite[x, y]]]] Execution time = 0 Seconds In[dfc6b]:= implies[member[pair[u,v],composite[x,y]],\ > member[v,image[x,image[y,singleton[u]]]]] composition Out[dfc6b]= equal[V, union[complement[image[V, > intersection[composite[x, y], singleton[pair[u, v]]]]], > image[V, intersection[image[x, image[y, singleton[u]]], singleton[v]]]]] Execution time = 0 Seconds In[dfc6c]:= implies[member[pair[u,v],composite[x,y]],\ > member[v,image[x,image[y,singleton[u]]]]] composition Out[dfc6c]= equal[V, union[complement[image[V, > intersection[composite[x, y], singleton[pair[u, v]]]]], > image[V, intersection[image[x, image[y, singleton[u]]], singleton[v]]]]] Execution time = 0 Seconds In[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 Out[dfc6d]= equal[V, union[complement[image[V, > intersection[cart[V, V], singleton[pair[u, v]]]]], > complement[image[V, intersection[image[x, image[y, singleton[u]]], > singleton[v]]]], image[V, > intersection[composite[x, y], singleton[pair[u, v]]]]]] Execution time = 0 Seconds In[dfc7a]:= implies[FUNCTION[z],subclass[z,cart[V,V]]] function Out[dfc7a]= True Execution time = 0 Seconds Axiom Group C In[axc1b]:= implies[INDUCTIVE[y],subclass[omega,y]] axiom of infinity Out[axc1b]= equal[V, union[complement[image[V, > intersection[omega, complement[y]]]], > complement[image[V, intersection[y, singleton[0]]]], > image[V, intersection[complement[y], image[SUCC, y]]]]] Execution time = 0 Seconds In[axc1c]:= member[omega,V] axiom of infinity Out[axc1c]= equal[V, image[V, singleton[omega]]] Execution time = 0 Seconds In[axc2]:= implies[member[x,V],member[U[x],V]] axiom of sum class Out[axc2]= equal[V, union[complement[image[V, singleton[x]]], > image[V, singleton[U[x]]]]] Execution time = 0 Seconds In[axc3]:= implies[member[x,V],member[P[x],V]] axiom of power class Out[axc3]= equal[V, union[complement[image[V, singleton[x]]], > image[V, singleton[P[x]]]]] Execution time = 0 Seconds In[axc4]:= implies[and[member[x,V],FUNCTION[z]],member[image[z,x],V]] axiom of replacement Out[axc4]= equal[V, union[complement[image[V, singleton[x]]], > image[V, intersection[z, complement[cart[V, V]]]], > image[V, intersection[complement[Id], composite[z, inverse[z]]]], > image[V, singleton[image[z, x]]]]] Execution time = 0 Seconds Axiom Group D In[axd1a]:= implies[not[equal[x,0]],\ > not[equal[0,intersection[x,P[complement[x]]]]]] axiom of regularity with Skolem function eliminated Out[axd1a]= equal[V, union[complement[image[V, x]], > image[V, intersection[x, P[complement[x]]]]]] Execution time = 0 Seconds Axiom Group E In[axe1]:= FUNCTION[CHOICE] axiom of universal choice Out[axe1]= equal[V, union[intersection[Id, cart[V, V]], > intersection[Id, complement[CHOICE]], > intersection[cart[V, V], > complement[composite[CHOICE, inverse[CHOICE]]]], > intersection[complement[CHOICE], > complement[composite[CHOICE, inverse[CHOICE]]]]]] Execution time = 0 Seconds In[axe2]:= subclass[CHOICE,inverse[E]] axiom of universal choice Out[axe2]= equal[V, union[complement[CHOICE], inverse[E]]] Execution time = 0 Seconds In[axe3]:= equal[domain[CHOICE],complement[singleton[0]]] axiom of universal choice Out[axe3]= equal[V, union[intersection[complement[domain[CHOICE]], > singleton[0]], intersection[complement[singleton[0]], domain[CHOICE]]]] Execution time = 0 Seconds In[axe4]:= implies[and[member[x,V],not[equal[x,0]]],\ > member[apply[CHOICE,x],x]] Quaife's formulation for axe2 and axe3 Out[axe4]= equal[V, union[complement[image[V, x]], > complement[image[V, singleton[x]]], > image[V, intersection[x, singleton[apply[CHOICE, x]]]]]] Execution time = 0 Seconds Total number of Axioms and Definitions: 60 Total Elapsed Time: 1 Seconds In[2]:= Exit