% problem-set/algebra/groups/order3.ver3.clauses % created : 07/22/86 % revised : 08/12/88 % description: % % Theorem: all groups of order 3 are isomorphic; i.e., if G1 and G2 each % have exactly three 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(c,g1). EL(c1,g2). EL(c2,g2). EL(c3,g2). -EL(x,g1) | EQUAL(x,a) | EQUAL(x,b) | EQUAL(x,c). -EL(x,g2) | EQUAL(x,c1) | EQUAL(x,c2) | EQUAL(x,c3). P(g1,a,a,a). P(g1,a,b,b). P(g1,b,a,b). P(g1,a,c,c). P(g1,c,a,c). P(g1,b,b,c). P(g1,b,c,a). P(g1,c,b,a). P(g1,c,c,b). P(g2,c1,c1,c1). P(g2,c1,c2,c2). P(g2,c2,c1,c2). P(g2,c1,c3,c3). P(g2,c3,c1,c3). P(g2,c2,c2,c3). P(g2,c2,c3,c1). P(g2,c3,c2,c1). P(g2,c3,c3,c2). % definition of a function k EQUAL(k(a),c1). EQUAL(k(b),c2). EQUAL(k(c),c3). % denial that k is an isomorphism EL(d1,g1). EL(d2,g1). EL(d3,g1). P(g1,d1,d2,d3). -P(g1,k(d1),k(d2),k(d3)).