% problem-set/algebra/category.theory/p13.ver1.in % created : 07/05/89 % revised : 07/05/89 % description: % % Lemma : dom(cod(x)) = cod(x). % representation: % % declare_predicate(3,P). % declare_predicates(2,[DEF,EQUAL]). % declare_predicate(1,IDENT). % declare_functions(1,[dom,cod]). % declare_function(2,star). % declare_constants([a,b,c,d,g,h]). % declare_variables([w,x,y,z,xy,yz,xyz,u,v,w]). % % IDENT(x) : x is an identity map % DEF(x,y) : the composition xy is defined % P(a,b,c) : identifies c as a composition (product) of a and b % dom(x) and cod(x) : functions to indicate domain and range of x % note that these are treated as functions, not objects, i.e. % dom(x) is the identity map on the domain of x % star(x,y) : skolem function from (all x all y (DEF(x,y) -> % exists z (P(x,y,z)))). % note that there are no special constants here; they're all used as % skolem constants in the denials of theorems set(ur_res). assign(max_seconds,1800). assign(max_mem,10000). list(axioms). % composition is closed when defined -DEF(x,y) | P(x,y,star(x,y)). % associative property -P(x,y,z) | DEF(x,y). -P(x,y,xy) | -DEF(xy,z) | DEF(y,z). % special category theory axiom -P(x,y,xy) | -P(y,z,yz) | -DEF(xy,z) | DEF(x,yz). -P(x,y,xy) | -P(xy,z,xyz) | -P(y,z,yz) | P(x,yz,xyz). -P(y,z,yz) | -DEF(x,yz) | DEF(x,y). -P(y,z,yz) | -P(x,y,xy) | -DEF(x,yz) | DEF(xy,z). -P(y,z,yz) | -P(x,yz,xyz) | -P(x,y,xy) | P(xy,z,xyz). -DEF(x,y) | -DEF(y,z) | -IDENT(y) | DEF(x,z). % properties of dom(x) and cod(x) IDENT(dom(x)). IDENT(cod(x)). DEF(x,dom(x)). DEF(cod(x),x). P(x,dom(x),x). P(cod(x),x,x). % definition of the identity predicate -DEF(x,y) | -IDENT(x) | P(x,y,y). -DEF(x,y) | -IDENT(y) | P(x,y,x). % equality axioms EQUAL(x,x). -EQUAL(x,y) | EQUAL(y,x). -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). % equality substitution axioms -EQUAL(x,y) | -P(x,z,w) | P(y,z,w). -EQUAL(x,y) | -P(z,x,w) | P(z,y,w). -EQUAL(x,y) | -P(z,w,x) | P(z,w,y). -EQUAL(x,y) | EQUAL(dom(x),dom(y)). -EQUAL(x,y) | EQUAL(cod(x),cod(y)). -EQUAL(x,y) | -IDENT(x) | IDENT(y). -EQUAL(x,y) | -DEF(x,z) | DEF(y,z). -EQUAL(x,y) | -DEF(z,x) | DEF(z,y). -EQUAL(x,y) | EQUAL(star(z,x),star(z,y)). -EQUAL(x,y) | EQUAL(star(x,z),star(y,z)). % composition is well defined -P(x,y,z) | -P(x,y,w) | EQUAL(z,w). end_of_list. list(sos). -EQUAL(dom(cod(A)),cod(A)). end_of_list.