%  problem-set/algebra/category.theory/p11.ver1.clauses
%  created : 07/05/89
%  revised : 07/05/89 

% description:
%
% Lemma : dom(dom(x)) = dom(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


%  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).

% denial of lemma

-EQUAL(dom(dom(A)),dom(A)).