% problem-set/topology/point.set/equality_ax.first_order % created : 08/08/88 % revised : 08/18/89 % equality axioms: all(x, eq_s(x,x)). all(x, eq_c(x,x)). all(x, eq_p(x,x)). all(x, all(y, eq_s(x,y) iff eq_s(y,x))). all(x, all(y, eq_c(x,y) iff eq_c(y,x))). all(x, all(y, eq_p(x,y) iff eq_p(y,x))). all(x, all(y, all(z, (eq_s(x,y) and eq_s(y,z)) imp eq_s(x,z)))). all(x, all(y, all(z, (eq_c(x,y) and eq_c(y,z)) imp eq_c(x,z)))). all(x, all(y, all(z, (eq_p(x,y) and eq_p(y,z)) imp eq_p(x,z)))). % equality substitution axioms, PREDICATES: all(x, all(y, all(z, (eq_c(x,y) and subset_c(x,z)) imp subset_c(y,z)))). all(x, all(y, all(z, (eq_s(x,y) and subset_s(z,x)) imp subset_s(z,y)))). all(x, all(y, all(z, (eq_s(x,y) and top_space(x,z)) imp top_space(y,z)))). all(x, all(y, all(z, (eq_c(x,y) and top_space(z,x)) imp top_space(z,y)))). all(x, all(y, (eq_c(x,y) and topology(x)) imp topology(y))). all(x, all(y, all(z, (eq_s(x,y) and el_s(x,z)) imp el_s(y,z)))). all(x, all(y, all(z, (eq_s(x,y) and el_p(z,x)) imp el_p(z,y)))). all(x, all(y, all(z, (eq_c(x,y) and el_s(z,x)) imp el_s(z,y)))). all(x, all(y, all(z, all(w, (eq_s(x,y) and open(x,z,w)) imp open(y,z,w))))). all(x, all(y, all(z, all(w, (eq_s(x,y) and open(z,x,w)) imp open(z,y,w))))). all(x, all(y, all(z, all(w, (eq_c(x,y) and open(w,z,x)) imp open(w,z,y))))). all(x, all(y, all(z, all(w, (eq_s(x,y) and closed(x,z,w)) imp closed(y,z,w))))). all(x, all(y, all(z, all(w, (eq_s(x,y) and closed(z,x,w)) imp closed(z,y,w))))). all(x, all(y, all(z, all(w, (eq_c(x,y) and closed(w,z,x)) imp closed(w,z,y))))). all(x, all(y, all(z, all(w, (eq_c(x,y) and finer(x,z,w)) imp finer(y,z,w))))). all(x, all(y, all(z, all(w, (eq_c(x,y) and finer(z,x,w)) imp finer(z,y,w))))). all(x, all(y, all(z, all(w, (eq_s(x,y) and finer(w,z,x)) imp finer(w,z,y))))). all(x, all(y, all(z, (eq_c(x,y) and basis(x,z)) imp basis(y,z)))). all(x, all(y, all(z, (eq_s(x,y) and basis(z,x)) imp basis(z,y)))). all(x, all(y, all(z, (eq_c(x,y) and subbasis(x,z)) imp subbasis(y,z)))). all(x, all(y, all(z, (eq_s(x,y) and subbasis(z,x)) imp subbasis(z,y)))). all(x, all(y, all(z, (eq_s(x,y) and hausdorff(x,z)) imp hausdorff(y,z)))). all(x, all(y, all(z, (eq_c(x,y) and hausdorff(z,x)) imp hausdorff(z,y)))). all(x, all(y, all(z, (eq_s(x,y) and tone(x,z)) imp tone(y,z)))). all(x, all(y, all(z, (eq_c(x,y) and tone(z,x)) imp tone(z,y)))). all(x, all(y, all(z, all(w, all(u, (eq_s(x,y) and neighborhood(x,z,w,u)) imp neighborhood(y,z,w,u)))))). all(x, all(y, all(z, all(w, all(u, (eq_p(x,y) and neighborhood(z,x,w,u)) imp neighborhood(z,y,w,u)))))). all(x, all(y, all(z, all(w, all(u, (eq_s(x,y) and neighborhood(w,z,x,u)) imp neighborhood(w,z,y,u)))))). all(x, all(y, all(z, all(w, all(u, (eq_c(x,y) and neighborhood(u,z,w,x)) imp neighborhood(u,z,w,y)))))). all(x, all(y, all(z, all(w, all(u, (eq_p(x,y) and limit_pt(x,z,w,u)) imp limit_pt(y,z,w,u)))))). all(x, all(y, all(z, all(w, all(u, (eq_s(x,y) and limit_pt(z,x,w,u)) imp limit_pt(z,y,w,u)))))). all(x, all(y, all(z, all(w, all(u, (eq_s(x,y) and limit_pt(w,z,x,u)) imp limit_pt(w,z,y,u)))))). all(x, all(y, all(z, all(w, all(u, (eq_c(x,y) and limit_pt(u,z,w,x)) imp limit_pt(u,z,w,y)))))). % equality substitution axioms, FUNCTIONS: all(x, all(y, all(z, eq_s(x,y) imp eq_s(inter_s(x,z),inter_s(y,z))))). all(x, all(y, all(z, eq_c(x,y) imp eq_c(inter_c(x,z),inter_c(y,z))))). all(x, all(y, eq_s(inter_s(x,y),inter_s(y,x)))). all(x, all(y, eq_c(inter_c(x,y),inter_c(y,x)))). all(x, all(y, eq_c(x,y) imp eq_s(sigma(x),sigma(y)))). all(x, all(y, all(z, eq_s(x,y) imp eq_s(rel_comp(x,z),rel_comp(y,z))))). all(x, all(y, all(z, eq_s(x,y) imp eq_s(rel_comp(z,x),rel_comp(z,y))))). all(x, all(y, eq_c(x,y) imp eq_c(top_of_basis(x),top_of_basis(y)))). all(x, all(y, eq_c(x,y) imp eq_c(top_of_subbasis(x),top_of_subbasis(y)))). all(x, all(y, all(z, all(w, eq_s(x,y) imp eq_s(subspace_top(x,z,w),subspace_top(y,z,w)))))). all(x, all(y, all(z, all(w, eq_c(x,y) imp eq_c(subspace_top(z,x,w),subspace_top(z,y,w)))))). all(x, all(y, all(z, all(w, eq_s(x,y) imp eq_s(subspace_top(z,w,x),subspace_top(z,w,y)))))). all(x, all(y, eq_s(x,y) imp eq_s(limit_pt_set(x),limit_pt_set(y)))). all(x, all(y, all(z, all(w, eq_s(x,y) imp eq_s(boundary(x,z,w),boundary(y,z,w)))))). all(x, all(y, all(z, all(w, eq_s(x,y) imp eq_s(boundary(z,x,w),boundary(z,y,w)))))). all(x, all(y, all(z, all(w, eq_c(x,y) imp eq_s(boundary(w,z,x),boundary(w,z,y)))))). all(x, all(y, all(z, all(w, eq_s(x,y) imp eq_s(interior(x,z,w),interior(y,z,w)))))). all(x, all(y, all(z, all(w, eq_s(x,y) imp eq_s(interior(z,x,w),interior(z,y,w)))))). all(x, all(y, all(z, all(w, eq_c(x,y) imp eq_s(interior(w,z,x),interior(w,z,y)))))). all(x, all(y, all(z, all(w, eq_s(x,y) imp eq_s(closure(x,z,w),closure(y,z,w)))))). all(x, all(y, all(z, all(w, eq_s(x,y) imp eq_s(closure(z,x,w),closure(z,y,w)))))). all(x, all(y, all(z, all(w, eq_c(x,y) imp eq_s(closure(w,z,x),closure(w,z,y)))))). % equality predicates: all(x, all(y, eq_s(x,y) iff (subset_s(x,y) and subset_s(y,x)))). all(x, all(y, eq_c(x,y) iff (subset_c(x,y) and subset_c(y,x)))).