Chapter 4

Method for Demonstration

4.1 Basic Method for Demonstration

We will explain the demonstration method. For a demonstration method, as we have explained before, we will first write a formula that needs to be demonstrated and then we will write the demonstration in between proof and end.

        A formula that is needs to be demonstrated
       proof
         · · ·
         · · ·
       thus (hence) ...;
       end;

The end of a demonstration will always finish with thus or hence.
    Let us demonstrate a proposition "p implies q".

     p implies q
        proof
          assume p;　　　　　　p is assumed
           · · ·
           · · ·
          thus q;　　　　　　　　q could be indicated
        end;

    First, we will initially write a formula "p implies q" that needs to be demonstrated, and write proof , end;. We do not need a semicolon after proof; however, there has to be one after end. If it is p, we need to demonstrate that it is q; however, p is also one logical formula. We will first write assume p and then p is assumed, and if we can indicate q, the demonstration is finished with thus q.
    Next, if we want to demonstrate "b=c implies a=b" after a=c is assumed, the following can be stated. With assume a=c, we will place label A:.


       A:a=c;
           b=c implies a=b
           proof
              assume B:b=c
              hence thesis by A;
           end;


    With assume ..., we hypothesize ... . In short, we indicate that it is a hypothesis section. Also, we should indicate that for hence ..., the last formula of this demonstration could be derived from a formula just before hence and the reasoning section of a hence formula. A thesis means that a formula should be indicated.
    Let's explain thus and hence a little in more detail.
    Although thus and hence are used in proof, the formula which should be proved becomes easy every time hence and thus appear and a proved part is removed from the formula connected by &. For example, the following is the proof of three formulas connected by and.


        theorem　3-1=2　&　5-2=3　&　6-3=3
        proof　2+1=3;
          hence　3-1=2 by REAL_2:17;
          3+2=5;
          hence　5-2=3　by REAL_2:17;
          3+3=6;
          hence thesis by REAL_2:17;
        end;


Since 3-1=2 are proved by the first hence, we become the formula which 5-2=3 & 6-3=3 should prove. Since 5-2=3 are proved by the next hence, 6-3=3 become the formula which should finally be proved. It means that all the remaining parts (6-3=3) are first proved by hence thesis.

    In addition, hence combines then and thus, as mentioned above.


        A1: A=B;
        A2: B=C;
        thus A=C by A1,A2;

For example, we can write the above as the following.

        A1: A=B;
        B=C;
        hence A=C by A1;