% problem-set/algebra/category.theory/p15.related.in % created : 07/07/89 % revised : 07/12/89 % description: % % Experiment to determine whether anything can be asserted to exist; % Theorem (exists x E(x)), denial (all x -E(x)). % representation: % % declare_predicates(2,[ee,=]). % declare_predicate(1,E). % declare_function(2,star). % declare_functions(1,[dom,cod]). % % ee(x,y) : equality restricted to E -- i.e., implying existence of x and y % x = y : ordinary classical equality (on all of M) % E(x) : x exists (provable/constructible) % 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(binary_res). set(hyper_res). set(ur_res). set(factor). set(para_into). set(para_from). set(para_from_right). set(para_from_left). set(dynamic_demod). set(dynamic_demod_all). set(order_eq). assign(max_seconds,1800). assign(max_mem,10000). set(delete_identical_nested_skolem). set(simplify_fol). formula_list(axioms). % equality axiom (all x (x = x)). end_of_list. formula_list(sos). % denial that anything at all exists (all x -E(x)). % Quaife has this written: (this looks really weird, but results from % having = here stand for equivalence, and it is a strange fact % from Scott's conception that all non-existent things are equivalent (all x all y ((x = y) | E(x) | E(y))). % restricted equality axioms (all x all y (ee(x,y) -> E(x))). (all x all y (ee(x,y) -> (x = y))). (all x all y ((E(x) & (x = y)) -> ee(x,y))). (all x all y (ee(x,y) -> E(y))). (all x all y (((E(x) & E(y)) & (x = y)) -> ee(x,y))). % category theory axioms (all x (E(dom(x)) -> E(x))). (all x (E(cod(x)) -> E(x))). (all x all y (E(star(x,y)) -> E(dom(x)))). (all x all y (E(star(x,y)) -> (dom(x) = cod(y)))). (all x all y ((E(dom(x)) & (dom(x) = cod(y))) -> E(star(x,y)))). (all x all y all z (star(x,star(y,z)) = star(star(x,y),z))). (all x (star(x,dom(x)) = x)). (all x (star(cod(x),x) = x)). (all x all y (E(star(x,y)) -> E(cod(x)))). end_of_list. list(demodulators). % (star(x,star(y,z)) = star(star(x,y),z)). (star(x,dom(x)) = x). (star(cod(x),x) = x). (dom(dom(x)) = dom(x)). (cod(dom(x)) = dom(x)). (dom(cod(x)) = cod(x)). (cod(cod(x)) = cod(x)). (dom(star(x,y)) = dom(y)). (cod(star(x,y)) = cod(x)). (star(dom(x),dom(x)) = dom(x)). (star(cod(x),cod(x)) = cod(x)). end_of_list.