The most basic rules for transforming formulas by predicate logic seem to be ALS and EXIST from the previous sections and ALIM and EXIM that will be introduced hereafter. Let us first mention some examples with the use of ALIM.

Example 1 a1 : (All x) (u imp f(x)) by ...;

Example 2 a1 : (All x) (All y) (t imp g (x,y))

by .....;...........

In short, if formulas that are quantitized with all symbols take the form of u imp f(x), and if that u is unrelated to a quantitization variable x (if it is a fixed number relating with x), it means that we can move all of the symbols right in front of the conclusion formula. These 2 formulas have definitely the same value; therefore, the opposite inference below is also possible. In this case, ALIM is also used.

Example 3 a1 : u imp (All x) (f(x)) by ...;

Example 4 a1 : t imp (All x) (All y) (g (x,y))

by ...;.........

Logical formula u imp f(x) has the same value with not u or f(x). Therefore, although the formation of ALIM is more obvious than the transformation below ( (**) signifies the same value),

it is easier to think in the following way. Therefore, we consider correspondence of the logical formula and the real number like below.

a and b ...... Min {a,b} a or b ...... Max {a,b} a imp b ...... a (<=) b (All x) (f(x)) ...... inf f(x)× (Exist x) (f(x)) .... sup f(x) ×

Then, ALIM corresponds with the formulas relating to the lower limit of the well known real numbers listed below.

For all x, u (<=) f(x) if and only if u (<=) inf f(x)

×

This formula is such an important one because it can definitely define the function inf. In the same way, the logical formula is considered to be as important as ALIM being able to define all of the symbols.

Similarly, EXIM corresponds with the following formula that is related to sup.

For all x, f(x) (<=) u if and only if sup f(x) (<=) u

×

In the case of EXIM, when the conclusion of the connotation formula is constant, all of the symbols hanging over the whole connotation formula can be transferred only to the subjunctive formula, and they will then change into exist symbols. Therefore, we provide these examples below.

Example 5 a1 : (All x) (f(x) imp u) by ...;

Example 6 a1 : (All x) (All y) (g(x,y) imp t) by ...;...........

Then, opposite of these will be guided by the same inference rules of EXIM.

Example 7 a1 : (Exist x) (f(x)) imp u by ...;

Example 8 a1 : (Exist x) (Exist y) (g(x,y)) imp t by ....; ..........

In addition, the structure of EXIM is also clear by such transformation of the formula below.

Thus, ALIM and EXIM are abbreviations of All-imp and Exist-imp.