% problem-set/algebra/groups/order2.ver3.clauses
% created : 07/22/86                          
% revised : 08/12/88                          

% description:
%
% Theorem: all groups of order 2 are isomorphic; i.e., if G1 has exactly
% two elements and G2 has exactly two elements, then there exists an
% isomorphism [a one-to-one and onto homomorphism] between them.
%
% The following are the usual axioms of a group with an additional argument 
% in the usual predicates and functions to identify the group.

% 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


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

%  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 groups 

EL(a,g1).
EL(b,g1).
EL(c1,g2).
EL(c2,g2).
-EL(x,g1)  |  EQUAL(x,a)  |  EQUAL(x,b).
-EL(x,g2)  |  EQUAL(x,c1) |  EQUAL(x,c2).
P(g1,a,a,a).
P(g1,a,b,b).
P(g1,b,a,b).
P(g1,b,b,a).
P(g2,c1,c1,c1).
P(g2,c1,c2,c2).
P(g2,c2,c1,c2).
P(g2,c2,c2,c1).

%  definition of a function k 

EQUAL(k(a),c1).
EQUAL(k(b),c2).

%  denial that k is an isomorphism 

EL(d1,g1).
EL(d2,g1).
EL(d3,g1).
P(g1,d1,d2,d3).
-P(g2,k(d1),k(d2),k(d3)).