% problem-set/algebra/category.theory/p7.ver3.clauses % created : 07/05/89 % revised : 07/07/89 % description : % % Theorem 7: If dom(x) and dom(y) exist, and dom(x) = cod(y), then % star(x,y) exists. % 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 % equality axioms (all x (x = 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))). % 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)). % axioms from Scott proven dependant by Quaife (with OTTER) % equality substitution axioms (Quaife uses paramodulation) % (all x all y (((x = y) & E(x)) -> E(y))). % (all x all y all z (((x = y) & ee(x,z)) -> ee(y,z))). % (all x all y all z (((x = y) & ee(z,x)) -> ee(z,y))). % (all x all y all z (((x = y) & (x = z)) -> (y = z))). % (all x all y all z (((x = y) & (z = x)) -> (z = y))). % (all x all y ((x = y) -> (dom(x) = dom(y)))). % (all x all y ((x = y) -> (cod(x) = cod(y)))). % (all x all y all z ((x = y) -> (star(x,z) = star(y,z)))). % (all x all y all z ((x = y) -> (star(z,x) = star(z,y)))). % restricted equality axioms % (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 all y (E(star(x,y)) -> E(cod(x)))). % axiom of indiscernibles (all x all y ((all z (E(z) -> ((x = z) <-> (y = z)))) -> (x = y))). % denial of theorem -(all x all y (((E(dom(x)) & E(dom(y))) & (dom(x) = cod(y))) -> E(star(x,y)))).