problem-set/algebra/groups/index.desc created : 07/09/86 revised : 08/15/88 Natural Language 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. Versions : index.ver1 : uses hyperresolution and a standard p-formulation. created : 7/9/86 from McCharen, Overbeek, & Wos [Aug. 1976]. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 08/15/88. index.ver2 : uses paramodulation and an equality formulation. created : 7/9/86 from McCharen, Overbeek, & Wos [Aug. 1976]. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : no proof in 5043 kept clauses.