4.8 Dividing into Cases

Next, we will discuss about demonstrating by dividing into cases. Let us assume that we want to demonstrate a proposition "A and B" and it can be done if we divide these into cases. For instance, we want to demonstrate by dividing into cases such as when x=1, x=2, and when x takes some other value. This means that with x=1,2, it becomes a peculiar point. At this point, it takes the structure of the following demonstrations.

L:( x=1 or x=2　or not ( x=1 & x=2 ))
now per cases by L;
case LA:x=1;
······
thus A and B;

case LB:x=2;
······
thus A and B;

case LC:not (x=1 & x=2);
······
thus A and B;

end;

We will demonstrate by supposing each case in "now per cases ~ end". We will demonstrate from "case x=1" to the beginning of "thus A and B" when x=1. In the same way, we will also demonstrate when x=2 and other cases. The sentences from now to end are considered as the whole one "A and B". For example, if we have then after "now ~ end", "then" receives the whole "now ~ end". Even though it is divided into each case with "case", the conclusion of each case is handed over to the end. Therefore, when all of this is cited, the fact that it was divided with "case" is forgotten and the fact that only the conclusions are the same is checked. Thus, it means that this is one formula.
In addition, since a formula like L is logically clear, there may not be "by L" of "now per cases by L.".