Ring Theory

A ring is a nonempty set R in which addition and multiplication are defined such that under addition the set is a commutative group and such that multiplication is associative and multiplication distributes over addition. The following clauses capture the properties of a ring.

EQ(sum(0,x),x).	EQ(x,x).
EQ(sum(x,0),x).	EQ(sum(x,y),sum(y,x))
EQ(sum(minus(x),x),0).	EQ(prod(prod(x,y),z),prod(x,prod(y,z))).
EQ(sum(x,minus(x)),0).	EQ(prod(x,sum(y,z)),sum(prod(x,y),prod(x,z))).
EQ(sum(sum(x,y),z),sum(x,sum(y,z))).	EQ(prod(sum(y,z),x),sum(prod(y,x),prod(z,x))).

Problem RT1, moderate. Prove that Boolean rings (rings in which the square of every x is x) are commutative.

EQ(prod(x,x),x).

Problem RT2, hard. Prove that rings in which the cube of every x is x are commutative.

EQ(prod(prod(x,x),x),x).

Problem RT3, hard. Prove that rings in which the fourth power of x is x are commutative.

EQ(prod(prod(prod(x,x),x),x),x).

Problem RT4, never proved in a single run unaided. Prove that rings in which the fifth power of x is x are commutative.

EQ(prod(prod(prod(prod(x,x),x),x),x),x).