3. 8 ORD(Order Exchange of Quantitization Symbols)

The exchanges between all of the successive symbols, or among the exist symbols (ORD is an abbreviation of order).

Example 1 a1 : (All x) (All y) (Exist z) (Exist u) (f(x,y,z,u)) by .... ;

a2 : (All y) (All x) (Exist u) (Exist z) (f(x,y,z,u)) by ORD (a1) ;

In the examples above, x, y, z, and u of both formulas a1 and a2 have to be in the same line of letters. In THEAX, (All w) (f(w)) and (All px) (f(px)) are generally considered to be the same formulas; however, ORD does not allow such identicality.

If we take the following detour, this rule will not be needed; however, the demonstration will be concise with it. It becomes the formula desired by a8 (a1 is the same with above).

a2 : (All y) (All x) (;
a3 : (Exist z) (Exist u) (f(x,y,z,u)) by ALS(a1) ;
a4 : (Exist p) (Exist q) (;
a5 : f(x,y,p,q) by FLW (a1) ;
a6 : (Exist u) (Exist z) (f(x,y,z,u)) by EXIST (a5) ;

) ;

a7 : (Exist u) (Exist z) (f (x,y,z,u)) by CNST (a4) ;/*CNST will be explained later*/) ;
a8 : (All y) (All x) (Exist u) (Exist z) (f(x,y,z,u)) by ARRN (a2) ;