Many-Valued Sentential Calculus

The axioms are the following, where the constant T can be interpreted as ``true'' and the functions i and n as implication and negation, respectively.

EQ(j(T,x),x).	EQ(i(i(x,y),y),i(i(y,x),x)).
EQ(i(i(x,y),i(i(y,z),i(x,z))),T).	EQ(i(i(n(x),n(y)),i(y,x)),T).

Problem MV1, simple. Prove that each of the following two equalities hold in many-valued sentential calculus.

EQ(i(n(n(x)),x),T).

EQ(i(x,n(n(x))),T).

Problem MV2, moderate. Prove that the following holds in the calculus.

EQ(i(i(x,y),i(i(z,x),i(z,y))),T).

Problem MV3, moderate. Prove that the following holds in the calculus.

EQ(i(i(x,y),i(n(y),n(x))),T).

Problem MV4, hard. Prove that the following holds in the calculus.

EQ(i(i(i(x,y),i(y,x)),i(y,x)),T).