% problem-set/algebra/category.theory/p15.ver2.in % created : 07/07/89 % revised : 07/07/89 % description: % % Axiom of Indiscernibles: (all z ((x=z) <-> (y=z))) -> (x=y). % representation: % % declare_predicate(2,=). % declare_function(2,star). % declare_functions(1,[dom,cod]). % % x = y : usual classical equality % star(x,y) : x composed with y % dom(x) : the object which is the domain of x % cod(x) : the object which is the codomain of x set(para_into). set(para_from). set(para_from_left). set(para_from_right). set(dynamic_demod). set(order_eq). assign(max_seconds,1800). assign(max_mem,10000). formula_list(axioms). % equality axiom (all x (x = x)). % category theory axioms (all x (cod(dom(x)) = dom(x))). (all x (dom(cod(x)) = cod(x))). (all x (star(dom(x),x) = x)). (all x (star(x,cod(x)) = x)). (all x all y ((cod(x) = dom(y)) -> (dom(star(x,y)) = dom(x)))). (all x all y ((cod(x) = dom(y)) -> (cod(star(x,y)) = cod(y)))). (all x all y all z (((cod(x) = dom(y)) & (cod(y) = dom(z))) -> (star(x,star(y,z)) = star(star(x,y),z)))). end_of_list. formula_list(sos). % denial of the axiom of indiscernibles -(all x all y ((all z ((x = z) <-> (y = z))) -> (x = y))). end_of_list. list(demodulators). (cod(dom(x)) = dom(x)). (dom(cod(x)) = cod(x)). (star(dom(x),x) = x). (star(x,cod(x)) = x). end_of_list.