%  problem-set/algebra/category.theory/p15.ver3.no4.in
%  created : 07/10/89
%  revised : 07/12/89

% description:
%
% Axiom of Indiscernibles: (all z (E(z) -> ((x=z) <-> (y=z)))) -> (x=y).
% from Scott's axioms alone.

% 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

set(binary_res).
set(factor).
set(ur_res).
set(hyper_res).
set(dynamic_demod).
set(dynamic_demod_all).
set(order_eq).
assign(max_seconds,3600).
assign(max_mem,10000).


formula_list(axioms).

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

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

% category theory axioms
% (all x all y (E(star(x,y)) -> E(cod(x)))).

end_of_list.


formula_list(sos).

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

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

% denial of the axiom of indiscernibles

(all z (E(z) -> ((a = z) <-> (b = z)))).
(a != b).

end_of_list.
