## 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) ;