% problem-set/algebra/groups/order3.ver4.clauses
% created : 07/22/86                                    
% revised : 08/15/88                                    

% description:
%
% Theorem: all groups of order 3 are isomorphic; i.e., if G1 and G2 each
% have exactly three elements, then there exists an isomorphism [a
% one-to-one and onto homomorphism] between them.
%
% Note: in order to prove the theorem, we specify one element of each group 
% as the identity element and take as a previously-proven lemma (obvious) 
% that maps from G1 -> G2 which are not one-to-one or which are not onto 
% need not be considered for isomorphisms between the groups.  Thus we 
% consider only the six one-to-one and onto maps between the groups, and 
% show that assuming none of them are homomorphisms gives a contradiction.

% representation:
%
% declare_predicates(2,[EL,EQUAL]).
% declare_predicate(4,[P]).
% declare_functions(1,[e,k,r,s,p1,p2,p3,q1,q2,q3]).
% declare_functions(2,[g,m]).
% declare_function(3,[f]).
% declare_constants([a,b,c,d,i,h,j,d1,d2,d3,G,G1,G2]).
% declare_variables([x,y,z,w,xg,yg,xy,yz,xyz]).
%
% EL(x,y) : x is an element of group y
% P(x,y,z,w) : in group x, the product of y and z is w
% e(x) : names the identity element of group x
% k(x) : names an isomorphism (see order2.ver3, order3.ver3)
% r(x) : is a possible isomorphism (see order2.ver4)
% s(x) : is a possible isomorphism (see order2.ver4)
% p1(x) : is a possible isomorphism (see order3.ver4)
% p2(x) : is a possible isomorphism (see order3.ver4)
% p3(x) : is a possible isomorphism (see order3.ver4)
% q1(x) : is a possible isomorphism (see order3.ver4)
% q2(x) : is a possible isomorphism (see order3.ver4)
% q3(x) : is a possible isomorphism (see order3.ver4)
% g(x,y) : in group x, names inverse of y
% m(x,y) : in group x, names an element which does not equal any power of
%	y; (see cyclic)
% f(x,y,z) : in group x, names the product of y and z
% i : identity element in group G named


% The following are the usual axioms of a group with an additional argument 
% in the usual predicates and functions to identify the group.

%  closure property 

-EL(x,xg)  | -EL(y,xg)  |  P(xg,x,y,f(xg,x,y)).
-EL(x,xg)  | -EL(y,xg)  |  EL(f(xg,x,y),xg).

%  the operation is well defined 

-P(xg,x,y,z)  | -P(xg,x,y,w)  |  EQUAL(w,z).
-P(xg,x,z,y)  | -P(xg,x,w,y)  |  EQUAL(w,z).
-P(xg,z,y,x)  | -P(xg,w,y,x)  |  EQUAL(w,z).

%  existence of identity 

EL(e(xg),xg).
P(xg,e(xg),x,x).
P(xg,x,e(xg),x).

%  existence of inverses 

-EL(x,xg)  |  EL(g(xg,x),xg).
P(xg,g(xg,x),x,e(xg)).
P(xg,x,g(xg,x),e(xg)).

%  associative property 

-P(xg,x,y,xy)  | -P(xg,y,z,yz)  | -P(xg,xy,z,xyz)  |  P(xg,x,xy,xyz).
-P(xg,x,y,xy)  | -P(xg,y,z,yz)  | -P(xg,x,yz,xyz)  |  P(xg,xy,z,xyz).

%  equality axioms 

EQUAL(x,x).
-EQUAL(x,y)  |  EQUAL(y,x).
-EQUAL(x,y)  | -EQUAL(y,z)  |  EQUAL(x,z).

%  equality substitution axioms 

-EQUAL(xg,yg)| -P(xg,x,y,z)  |  P(yg,x,y,z).
-EQUAL(x,y)  | -P(xg,x,z,w)  |  P(xg,y,z,w).
-EQUAL(x,y)  | -P(xg,w,x,z)  |  P(xg,w,y,z).
-EQUAL(x,y)  | -P(xg,w,z,x)  |  P(xg,w,z,y).
-EQUAL(xg,yg)|  EQUAL(f(xg,x,y),f(yg,x,y)).
-EQUAL(x,y)  |  EQUAL(f(xg,x,z),f(xg,y,z)).
-EQUAL(x,y)  |  EQUAL(f(xg,z,x),f(xg,z,y)).
-EQUAL(xg,yg)|  EQUAL(g(xg,x),g(yg,x)).
-EQUAL(x,y)  |  EQUAL(g(xg,x),g(xg,y)).
-EQUAL(xg,yg)| -EL(x,xg)  |  EL(x,yg).
-EQUAL(x,y)  | -EL(x,xg)  |  EL(y,xg).
-EQUAL(xg,yg)|  EQUAL(e(xg),e(yg)).

% definition of the two different groups of order 3
% at least three:

-EQUAL(G1,G2).
EL(a,G1).
EL(b,G1).
EL(c,G1).
-EQUAL(a,b).
-EQUAL(c,a).
-EQUAL(b,c).
EL(d,G2).
EL(h,G2).
EL(j,G2).
-EQUAL(d,h).
-EQUAL(j,d).
-EQUAL(h,j).

% only three:

-EL(x,G1)  |  EQUAL(x,a) |  EQUAL(x,b) |  EQUAL(x,c).
-EL(x,G2)  |  EQUAL(x,d) |  EQUAL(x,h) |  EQUAL(x,j).

% a is the identity element of G1, d is the identity element of G2

EQUAL(e(G1),a).
EQUAL(e(G2),d).
P(G1,a,x,x).
P(G1,x,a,x).
P(G2,d,x,x).
P(G2,x,d,x).

%  definition of maps p1, p2, p3, q1, q2, q3, six possible isomorphisms

EQUAL(p1(a),d).
EQUAL(p1(b),h).
EQUAL(p1(c),j).
EQUAL(p2(a),d).
EQUAL(p2(b),j).
EQUAL(p2(c),h).
EQUAL(p3(a),h).
EQUAL(p3(b),d).
EQUAL(p3(c),j).

EQUAL(q1(a),h).
EQUAL(q1(b),j).
EQUAL(q1(c),d).
EQUAL(q2(a),j).
EQUAL(q2(b),h).
EQUAL(q2(c),d).
EQUAL(q3(a),j).
EQUAL(q3(b),d).
EQUAL(q3(c),h).

% equality substitution axioms for p1, p2, p3, q1, q2, q3

-EQUAL(x,y) | EQUAL(p1(x),p1(y)).
-EQUAL(x,y) | EQUAL(p2(x),p2(y)).
-EQUAL(x,y) | EQUAL(p3(x),p3(y)).
-EQUAL(x,y) | EQUAL(q1(x),q1(y)).
-EQUAL(x,y) | EQUAL(q2(x),q2(y)).
-EQUAL(x,y) | EQUAL(q3(x),q3(y)).

-EQUAL(x,p1(z)) | -EQUAL(y,p1(z)) | EQUAL(x,y).
-EQUAL(x,p2(z)) | -EQUAL(y,p2(z)) | EQUAL(x,y).
-EQUAL(x,p3(z)) | -EQUAL(y,p3(z)) | EQUAL(x,y).
-EQUAL(x,q1(z)) | -EQUAL(y,q1(z)) | EQUAL(x,y).
-EQUAL(x,q2(z)) | -EQUAL(y,q2(z)) | EQUAL(x,y).
-EQUAL(x,q3(z)) | -EQUAL(y,q3(z)) | EQUAL(x,y).


%  denial that one of p1,p2,p3,q1,q2,q3 is a homomorphism 

EL(d1,G1).
EL(d2,G1).
EL(d3,G1).
P(G1,d1,d2,d3).
-P(G1,p1(d1),p1(d2),p1(d3)) | -P(G1,p2(d1),p2(d2),p2(d3)) | 
	-P(G1,p3(d1),p3(d2),p3(d3)) | -P(G1,q1(d1),q1(d2),q1(d3)) | 
	-P(G2,q2(d1),q2(d2),q2(d3)) | -P(G3,q3(d1),q3(d2),q3(d3)).


EQUAL(g(xg,e(xg)),e(xg)).
EQUAL(f(xg,x,g(xg,x)),e(xg)).
EQUAL(f(xg,g(xg,x),x),e(xg)).
EQUAL(g(xg,f(xg,x,y)),f(xg,g(xg,x),g(xg,y))).
EQUAL(f(xg,x,f(xg,g(xg,x),y)),y).
EQUAL(f(xg,g(xg,x),f(xg,x,y)),y).
EQUAL(f(xg,f(xg,x,y),z),f(xg,x,f(xg,y,z))).