%  problem-set/algebra/groups/index.ver1.clauses
%  created : 07/09/86                                            
%  revised : 08/15/88                                       
                                                          
% description:
%
% Theorem: all subgroups of index 2 are normal; i.e., if O is a 
% subgroup of G and there are exactly 2 cosets in G/O, then O
% is normal [that is, for all x in G and y in O, x*y*inverse(x) is
% back in O].
%
% NOTE: Used to define a subgroup of index two is a theorem which says that
% {for all x, for all y, there exists a z such that if x and y are both not
% in the subgroup O, then z is in O and x*z=y} if & only if {O has index 2
% in G}.  This z is named by the skolem function i(x,y).
%
% Explanation: If O is of index two in G, then there are exactly two 
% cosets, namely O and uO for some u not in O.  If both of x and y are not
% in O, then they are in uO.  But then xO=yO, which implies that there
% exists some z in O such that x*z=y.  If the condition holds that {for all 
% x, for all y, there exists a z such that if x and y are both not in the 
% subgroup O, then z is in O and x*z=y}, then xO=yO for all x,y not in O,
% which implies that there are at most two cosets; and there must be at
% least two, namely O and xO, since x is not in O.  Therefore O must be of
% index two.

% representation:
%
% declare_predicate(1,[O]).
% declare_predicate(2,[EQUAL]).
% declare_predicate(3,[P]).
% declare_functions(1,[g,k]).
% declare_functions(2,[f,l]).
% declare_constants([e,a,b,c,d,h,j,k]).
% declare_variables([x,y,z,u,v,w]).
%
% O(x) : used for membership in a subgroup of index 2 (see index)
% P(x,y) : product of x and y is z
% g(x) : inverse of x
% k(x) : used to name some inverse of x (see ident2)
% f(x,y) : names the product of x and y
% l(x,y) : names an element of the subgroup of index 2 (see index)
% e : identity element


%  existence of identity    

P(e,x,x).
P(x,e,x).

%  existence of inverse  

P(g(x),x,e).
P(x,g(x),e).

%  closure  

P(x,y,f(x,y)).

%  associative property  

-P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w).
-P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w).

%  the operation is well defined  

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

%  equality axioms  

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

%  equality substitution axioms  

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


%  Definition of subgroup of index 2 

 O(e).
-O(x) | O(g(x)).
-O(x) | -O(y) | -P(x,y,z) | O(z).
O(x) | O(y) | O(l(x,y)).
O(x) | O(y) | P(x,l(x,y),y).

% equality sub. axioms for new predicate & function

-EQUAL(x,y) | -O(x) | O(y).
-EQUAL(x,y) | EQUAL(l(w,x),l(w,y)).
-EQUAL(x,y) | EQUAL(l(x,w),l(y,w)).

%  Denial of the theorem    

O(b).
P(b,g(a),c).
P(a,c,d).
-O(d).