%  problem-set/algebra/category.theory/p15.related.clauses
%  created : 07/07/89
%  revised : 07/12/89

% description:
%
% Experiment to determine whether anything can be asserted to exist;
% Theorem (exists x E(x)), denial (all x -E(x)).

% 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 axiom
(all x (x = x)).

% denial that anything at all exists
(all x -E(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))).
(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 (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)).
(all x all y (E(star(x,y)) -> E(cod(x)))).


(dom(dom(x)) = dom(x)).
(cod(dom(x)) = dom(x)).
(dom(cod(x)) = cod(x)).
(cod(cod(x)) = cod(x)).
(dom(star(x,y)) = dom(y)).
(cod(star(x,y)) = cod(x)).
(star(dom(x),dom(x)) = dom(x)).
(star(cod(x),cod(x)) = cod(x)).