## 3. 12 SUBST (Substitution)

In the mathematical system, the concept of substitution is as important as the concept of logic. In reality, this dispositional program is complicated. This is because depending on the form of formulas, substitution is possible. For traditional mathematics, people tacitly knew the correct way to substitute. For example, we can not put a formula b + c = d into a formula ab + c as a substitution but into a formula a+b+c. It is because people knew mathematical background such as the fact that multiplication is stronger than addition or that combination rule for addition is formed. Thus, substitution definitely is not a simple rearrangement of letter lines. We cannot altogether laugh at elementary students for often substituting incorrectly. It is strange that traditional mathematicians did not pay too much attention to substitution even though it is more important than logic.

Substitution is done by a rule called SUBST. Here are some examples below.

Example 1 a1 : [a=b] by .... ;

a2 : (All x) (f(x,a)) by .... ;
.........
a3 : (All x) (f(x,b)) by SUBST (a2,a1) ;

Example 2 a1 : [a and b=c] by .... ;

a2 : c and f(c) or a and b by ... ;
.........
a3 : a and b and f(c) or c by SUBST (a2,a1) ;

In example 2, c in a2 is replaced by a and b, simultaneously a and b are superseded by c. In such ways, it is acceptable to fully take advantage of the fact that a and b = c.

Also, there is an argument order. It is an understood fact that the latter formula of the argument is substituted to the former formula of the argument.

It is the same with the traditional substitution in mathematics where the consideration of the operation order is required. However, we need to pay careful attention because the combination rule of operation is not considered. For instance, these are wrong examples.

Example (wrong) a1 : [b and c=a] by .... ;

a2 : d and b and c by .... ;
..........
a3 : d and a by SUBST (a2,a1) ;

Example (wrong) a1 : [b and c=a] by .... ;

a2 : d and a by.... ;
..........
a3 : d and b and c by SUBST (a2,a1) ;