% problem-set/algebra/category.theory/p6.ver3.clauses % created : 07/07/89 % revised : 07/19/89 % description: % % Theorem 6: cod(x) is the unique identity j such that jx is defined % 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: d is an identity which is not cod(a) E(star(d,a)). -E(star(x,d)) | (star(x,d) = x). -E(star(d,x)) | (star(d,x) = x). (cod(a) != d).