Let us think why Russel's paradoxes were born and if there are ways to avoid them. As to the causes of paradoxes being born, the following can be stated.
1. Axiom being inadequate.
2. Logic being inadequate. Therefore, logic that do not form the law of the excluded middle should be used.
3. Unfit variables of functions are being applied.
Regarding 1, there are examples which cause us to think that the axiom is not the only origin. That is,
010 'Text Paradox-2;
020 'Lemma; A:False;
030 'Proof;a0: Put G(h,g)=h(g);
040 ' a1: Put f(x)=not G(x,x);
050 ' a2: Put A=f;
060 ' a3: G(A,A) imp;
070 ' a4: G(f,A) by SUBST(a3,a2);
080 ' a5: f(A) by FUNF(a0,a4);
090 ' imp not G(A,A) by FUNF(a1,a5);
100 ' a6: not G(A,A) imp;
110 ' a7: f(A) by FUNF(a1,a6);
120 ' a8: G(f,A) by FUNF(a0,a7);
130 ' imp G(A,A) by SUBST(a8,a2);
140 ' a9: False by LOGIC(a3,a6);
160 'End Text;
When it is written this way, the form f(f) does not appear. Therefore, when it is checked by the system, the message "Proof is complete" comes out. Despite the fact that this text does not possess an axiom, paradoxes arise.
Therefore, it is hasty to blame the axiom of the set theory for Russel's paradoxes. We need to consider the situation above of f(f) appearing substantially. Consequently, the possibility of the third cause is significant. In reality, Russel's paradoxes also takes the form f(A) for the 120th line of formula a5; however, when a2 : A = Set (f) is substituted, it becomes f(Set(f)). This form should be repelled by the system's review.
Substantially, we tend to think that we should automatically check for the form f(f) or f(...(f)...); however, this is more difficult than we think. Cases of examples above and Russel's paradoxes are simpler. For the examples above, A = f is obvious for formula a2; however, it is difficult to see through f=A when it is expressed indirectly like B=f and A=B. If we desire, it is possible to make such complicated paradoxes that need a tremendous amount of demonstrations to acquire f=A. To see through these, it is thought to be a very difficult technique to automatically demonstrate all the demonstrations. Therefore, now, there is no other way than to look for the form f(f) when False is demonstrated. To be bad intentioned, it is also possible to skillfully hide paradoxes during the usual theorem demonstrations. That way, any propositions can be certainly demonstrated.
That is a distressing problem for the operation of the system; however, it is not a serious problem for the mathematical system. There are some similarities of the problems of paradoxes and taking measures to avoid hauling of mikes and speakers. It is difficult to accurately predict when the noise comes out when mikes and speakers are close together. When it makes a noise, the simplest solution is to move the mikes and speakers away from each other (it would be difficult for places like theaters, but if we suppose some malicious people bringing in special reverberation boads, it is difficult to take adequate measures) . If we use the speaker device knowing that it may make some noises, it will be helpful.
Let us examine the second cause above in the next section.