Let us write down Russel's paradoxes in the THEAX language. To do that, the concept of a set must be postulated. Assuming that strict postulation calls for many different kinds of arguments, we need to think of the minimal proposition necessary for the set and try postulating that tentatively. First, the following operation to make the set A from the logical proposition P must be given.

A= {x : P(x)}

This can be thought of as an image given to correspond to the logical proposition P with the set A. If we call this image "Set", the following can be written.

A= Set(P)

Moreover, the proposition saying that "the formal x belongs with the set A" indicated below must be given.

x(c)A

This is thought as the predicate proposition of x which was decided through subordination to A and naming that predicate proposition Bel (abbreviation of Belong), x (c)A of above can be written like the following.

Bel (A) (x)

Therefore, Set and Bel, or the concepts that correspond with these are necessary for the set theory. In addition, in between these concepts, axiom formulas that correspond with the following formulas must be structured such as the self-evident one below.

x (c){z : P(z)} is equivalent to P (x)

Regardless of this being an axiom or not, this must be structured. The following formula corresponds with this formula.

Bel (Set (P)) (x) eqv P(x)

Under the text below, when postulating this with the two formulas of SETQ and SETR, Russel's paradoxes can be written as Lemma.

020 'Axiom; Bel,Set;

030 ' Formulae; SETQ: (All f)(All x)(Bel(Set(f))(x)imp f(x));

040 ' SETR: (All f)(All x)(f(x)imp Bel(Set(f))(x));

050 'End Axiom;

060 '

070 'Lemma; A: False;

080 'Proof; a1: Put f(x)=not Bel(x)(x);

090 ' a2: Put A=Set(f);

100 ' a3: Bel(A)(A) imp; /* If A belongs to A */

110 ' a4: Bel(Set(f))(A) by SUBST(a3,a2);

120 ' a5: f(A) by ALS(SETQ,a4);

130 ' imp not Bel(A)(A) by FUNF(a1,a5);

140 ' a6: not Bel(A)(A) imp; / *If A does not belong to A */

150 ' a7: f(A) by FUNF(a1,a6);

160 ' a8: Bel(Set(f))(A) by ALS(SETR,a7);

170 ' imp Bel(A)(A) by SUBST(a8,a2);

180 ' a9: False by LOGIC(a3,a6);

190 'Q.E.D.(a9);

200 'End Text;

When verificating this text with the THEAX system, such indication as below appears on the screen saying that it is not wrong.

Error Count= 0 ecode= 0

Proof is complete. (Tested by THEAX ver1.0)

The reason why this demonstration did not get caught by the check explained in the previous sections is because apparently, the form x(x) did not appear. That is due to the fact that it is hidden in the form f(A) of a5 and a7. Because A = Set(f), f(A) originally takes the form of f(Set(f)). Therefore, f of itself appears on the variables of f.