% problem-set/algebra/groups/index.ver2.clauses
% created : 07/21/86                                  
% revised : 08/12/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_function(1,[g]).
% declare_functions(2,[f,l]).
% declare_constants([e,a,b,c,d,h,j,k]).
% declare_variables([x,y,z]).
%
% O(x) : membership in a subgroup of index 2 (see index)
% g(x) : inverse of x
% f(x,y) : names the product of x and y
% l(x,y) : names an element in O (see index)
% e : identity element


% For any x and y in the group x*y is also in the group.  No clause is needed 
% here since this is an instance of reflexivity given as EQUAL(x,x).                   
% There exists an identity element 'e' defined below.   
% left identity  

EQUAL(f(e,x),x).

% right identity 

EQUAL(f(x,e),x).

% for any x in the group, there exists an element y such that x*y = y*x = e. 
% left inverse 

EQUAL(f(g(x),x),e).

% right inverse 

EQUAL(f(x,g(x)),e).

% the operation '*' is associative  

EQUAL(f(f(x,y),z),f(x,f(y,z))).

% the operation '*' is well-defined.  No clause is needed here since this 
% is an instance of reflexivity given as EQUAL(x,x).                           

% reflexivity 

EQUAL(x,x).


% Definition of a subgroup of index 2    

O(e).
-O(x) | O(g(x)) .
-O(x) | -O(y) | -EQUAL(f(x,y),z) | O(z) .
O(x) | O(y) | O(i(x,y)) .
O(x) | O(y) | EQUAL(f(x,i(x,y)),y) .


% The following clauses deny that O is a normal subgroup 

O(b).
EQUAL(f(b,g(a)),c).
EQUAL(f(a,c),d).
-O(d).