Traditionally, one of the themes for basic mathematical theory was to evade inconsistencies. Russel's famous paradox became a warning against the simple set theory. There were many attempts at the axiom set theory afterwards; however, all of them are difficult. THEAX also cannot escape the danger of paradoxes. For instance, let us look at the following inference.

010 'Text Paradox;

020 'Lemma; A1: False;

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

040 ' a2: f(f) imp;

050 ' imp not f(f) by FUNF(a1,a2);

060 ' a3: not f(f)imp;

070 ' imp f(f) by FUNF(a1,a3);

080 ' a4: False by LOGIC(a2,a3);

090 'Q.E.D.(a4);

100 'End Text;

In such ways, by defining such a function as f(x)=not x(x), it looks as if the falseness was proved like formula a4. This is thought to be the most simple form of consistency. Aren't all of Russel's and others' paradoxes this transformation? THEAX avoids the above inference from being justified by following the rules below. Therefore, the inferences are considered to be wrong if the form of f(f) appears because of ALS (also FUNF) or SUBST. That evidence is due to this: "even if it says all x, 'all' does not mean including myself". Therefore, if we check the above text by the THEAX system, the following message appears on the screen.

*FUNF inference error(in funf) ecode= 10220*

*in logical line ending at 050*

*FUNF inference error(in funf) ecode= 10220*

*in logical line ending at 070*

*Error Count= 2 ecode= 10220*

Therefore, lines 50 and 70 are wrong. Here, please note that the form x(x) in line 30 is not wrong. It is not wrong to just write the recursive form.

Further, the form f(f) is different from the one below.

f(f(x))

The latter can be made freely with ALS or SUBST. In addition, the following form is also not permitted.

f(a,b) (c,g(f)) (x)

It is because f has become a variable of f as a result.

The way of considering THEAX's avoidance of inconsistency all depends on the examples above. It is thought to be that all other kinds of paradoxes can be avoided with these examples. However, despite the fact that the form x(x) is utilized in reality, it is possible to write as if it does not exist (discussed later). Therefore, the current THEAX system (Ver.1.0) is omitted and the message "Proof is complete" appears. The program to avoid omission becomes complicated and difficult. As a result, we will currently establish the rule that functions like x(x) or x(...(x)) can not possess variables of themselves and substantially, this rule must not be broken. Substantially means that when x = y is understood, such a way of taking variables like x(y) is also not permitted. However, in the latter case, even if such rules are given, the current program can not check for the rule violations.