Appendex 2 The Theory of Groups

Page 1


00010'Text Group;

00020'Definition;/* Binary-Algebra,Semigroup,Monoid,Group */

00030' AlDe1: Put Binary-Op(S)(f)=(All x)(All y)(S(x)and S(y)imp S(f(x,y)));

00040' AlDe2: Put Binary-Algebra(S,f)=Binary-Op(S)(f);

00050' AlDe3: Put Associative(S)(f)=Binary-Op(S)(f)and (All x)(All y)(All z)

00060' (S(x)and S(y)and S(z)imp[f(x,f(y,z))=f(f(x,y),z)]);

00070' AlDe4: Put Semigroup(S,f)=Associative(S)(f);

00080' AlDe5: Put Left-Identity(S,f)(l)=S(l)and (All x)(S(x) imp[f(l,x)=x]);

00090' AlDe6: Put Right-Identity(S,f)(r)=S(r)and (All x)(S(x)imp[f(x,r)=x]);

00100' AlDe7: Put Identity(S,f)(e)=Left-Identity(S,f)(e)and Right-Identity

00110' (S,f)(e);

00120' AlDe8: Put Monoid(S,f,e)=Semigroup(S,f)and Identity
(S,f)(e);

00130' AlDe9: Put Commutative(S,f)=(All x)(All y)(S(x)and S(y)imp[f(x,y)=f(y,

00140' x)]);

00150' AlDe10: Put Left-Zero(S,f)(a)=(All x)(S(x)imp[f(a,x)=a]);

00160' AlDe11: Put Right-Zero(S,f)(b)=(All x)(S(x)imp[f(x,b)=b]);

00170' AlDe12: Put Zero(S,f)(c)=Left-Zero(S,f)(c)and Right-Zero(S,f)(c);

00180' AlDe13: Put Group(S,f,e,Iv)=Monoid(S,f,e)and(All x)(S(x)imp S(Iv(x))

00190' and[f(x,Iv(x))=e]and[f(Iv(x),x)=e]);

00200'End Def;

00210'

00220'Lemma;/* Left-Identity and Right-Identity coincide.*/

00230' AlLem1: (All S)(All f)(All u)(All v)(Left-Identity(S,f)(u)and

00240' Right-Identity(S,f)(v)imp [u=v]and Identity(S,f)(u));

00250'Proof;

00260' a1:(All S)(All f)(All u)(All v)(;

00270' a2: Left-Identity(S,f)(u)and Right-Identity(S,f)(v)imp;

00280' a3: Left-Identity(S,f)(u) by LOGIC(a2);

00290' a4: S(u)and (All x)(S(x)imp[f(u,x)=x]) by FUNF(AlDe5,a3);

00300' a5: (All x)(S(x)imp[f(u,x)=x]) by LOGIC(a4);

00310' a6: S(v)imp[f(u,v)=v] by ALS(a5);

00320' a8: Right-Identity(S,f)(v) by LOGIC(a2);

00330' a9: S(v)and(All x)(S(x)imp[f(x,v)=x]) by FUNF(AlDe6,a8);