% problem-set/algebra/rings/commute.ver3.clauses % created : 07/09/86 % revised : 07/13/88 % description : % % Theorem: If for all x, (x * x) = x, then the ring is commutative % under multiplication; i.e., for all x and y, (x * y) = (y * x). % representation : % % S means sum, P means product; j(x,y) is the sum of x and y, f(x,y) % is the product of x and y; g(x) is the additive inverse of x; 0 is % the additive identity element; a,b,c,d are constant ring elements. % % declare_predicates(3,[S,P]). % declare_predicate(2,EQUAL). % declare_functions(2,[j,f]). % declare_function(1,g). % declare_constants([0,a,b,c,d]). % declare_variables([x,y,z,u,v,w,v1,v2,v3,v4]). % Left identity S(0,x,x). % Right identity S(x,0,x). % Left inverse S(g(x),x,0). % Right inverse S(x,g(x),0). % Associative property -S(x,y,u) | -S(y,z,v) | -S(u,z,w) | S(x,v,w). -S(x,y,u) | -S(y,z,v) | -S(x,v,w) | S(u,z,w). % Closure property S(x,y,j(x,y)). % Well definedness of addition -S(x,y,u) | -S(x,y,v) | EQUAL(u,v). % Addition is commutative -S(x,y,z) | S(y,x,z). % 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). % Closure of multiplication P(x,y,f(x,y)). % Well definedness of multiplication -P(x,y,u) | -P(x,y,v) | EQUAL(u,v). % Distributivity axioms -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -P(x,v3,v4) | S(v1,v2,v4). -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(x,v3,v4). -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -P(v3,x,v4) | S(v1,v2,v4). -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(v3,x,v4). % Reflexivity EQUAL(x,x). % Symmetry -EQUAL(x,y) | EQUAL(y,x). % Transitivity -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). % Equality substitution axioms -EQUAL(u,v) | -S(u,x,y) | S(v,x,y). -EQUAL(u,v) | -S(x,u,y) | S(x,v,y). -EQUAL(u,v) | -S(x,y,u) | S(x,y,v). -EQUAL(u,v) | EQUAL(g(u),g(v)). -EQUAL(u,v) | EQUAL(j(u,x),j(v,x)). -EQUAL(u,v) | EQUAL(j(x,u),j(x,v)). -EQUAL(u,v) | -P(u,x,y) | P(v,x,y). -EQUAL(u,v) | -P(x,u,y) | P(x,v,y). -EQUAL(u,v) | -P(x,y,u) | P(x,y,v). -EQUAL(u,v) | EQUAL(f(u,x),f(v,x)). -EQUAL(u,v) | EQUAL(f(x,u),f(x,v)). % the ring is boolean P(x,x,x). % denial of the theorem P(a,b,c). -P(b,a,c).