defAs(in,p1). % the only map letter which is really needed: membership defAs(form(P),syq(rev(P),in)). --'{\\bf : set-formation construct}'. defAs(ni,rev(in)). % reverse of membership 'Coll'(form(ni)). --'{\\bf : extensionality axiom}'. defAs(ur,diag(form(id))). --' : under the above axioms, individuals cannot exist'. defAs(notni,opp(ni)). --' : under the above axioms, individuals cannot exist'. 'Tot'(setminus( setminus( un(dagger(un(notni,lA(ur)),0),ni),circ(circ(ni,setminus(id,ur)),in)), lA(ur))). --' : regularity axiom'. defAs(funcPart(Q),setminus(Q,circ(Q,di))). % "functional part" operator defAs(unHas,circ(ni,ni)). % 2nd "belongs to something which belongs to" 1st defAs(nunHas,circ(ni,opp(ni))). % 2nd "does not belong to all elements of" 1st defAs(mix,int(unHas,nunHas)). % "mix" predicate defAs(sn,funcPart(mix)). % left quasi-projection % pairing axiom (encompassing null-set axiom, and both single-element addition and removal) u_circ(in,sn). --'{\\bf : axiom of elementary sets}'. defAs(dxx,circ(int(ni,circ(opp(circ(mix,di)),in)),sn)). % right quasi-projection 'Maddux'(tot(sn),tot(dxx),setMaddux). --': one way of incorporating full first-order notation'. %%TEST: %% translquant(ax_sets,setMaddux,biimp(all([1],neg(@(p3,1,2))),equiv(p3,p4)),Q) %% i.e., %% quantifmla(biimp(all([1],neg(@(p3,1,2))),equiv(p3,p4)),Psi), %% mapeq(setMaddux(Psi),[ax_sets],Q). defAs(circum(P),rR(in,rev(P))). --' : circumscription construct'. 'Tot'(circum(unHas)). --'{\\bf : unionset axiom}'. defAs(powHas,lR(ni,ni)). % "powerset" predicate 'Tot'(circum(powHas)). --'{\\bf : powerset axiom}'. defAs(separat(P,Q),int(circ(funcPart(Q),ni),P)). % "separation" predicates 'Tot'(form(separat(P,Q))). --'{\\bf : subset axioms}'. defAs(trans,diag(circum(unHas))). 'Tot'(circ(in,trans)). --' : transitive embedding axiom'. 'Tot'(circum(circ(sibs([sn,circ(sn,in),dxx]),funcPart(Q)))). --' : replacement axioms'. 'Tot'(lA(setminus(setminus(setminus(int(int(circum(unHas), rev(circum(unHas))),di),in),ni),circ(circ(ni,opp(symm(in,ni))),in)))). --' : infinity axiom'. defAs(meets,bros(in)). % "intersects" predicate defAs(splits,setminus(rR(meets,ni),rA(int(ni,circ(ni,int(meets,di)))))). 'Tot'(setminus(un(opp(rA(splits)),splits),circ(splits,int(rev(powHas),di)))). --' : choice axiom'. % plenitude: all( x, exs(y, and(ur(y,y),neg(exs(v,and(in(v,x),in(y,v)))) )). setMaddux(neg( exs([1], neg( exs([2], and(@(ur, 2, 2), neg( exs([3], and(@(ni, 1, 3),@(in, 2, 3)), [1, 2]))), [1])), []))).