%  problem-set/algebra/category.theory/p5.ver3.clauses
%  created : 07/07/89
%  revised : 07/07/89

% description:
%
% Theorem 5: dom(x) is the unique identity i such that xi 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 the theorem:  d is an identity not equal to dom(a)

E(star(a,d)).
-E(star(x,d)) | (star(x,d) = x).
-E(star(d,y)) | (star(d,y) = y).
(dom(a) != d).