4.6 All Symbols

We will now discuss about a predicate proposition. Let us demonstrate for x holds p[x] & q[x]. Further, p[x] means a predicate that includes x and it does not mean that brackets are permitted.



  for x holds P[x] & Q[x]



   proof



    let x;



     ......



     ......



    thus P[x];



     ......



     ......



    thus Q[x];  (thesis)



   end;

The word let exists as an opposite of for from all symbols. P is demonstrated by thus P[x] with leaving let x as it is. Further, we will demonstrate Q with Q[x].

If it does not get confused, this letter can be changed. For example, the letter can be changed to y.

4.6.1 When There Are Two Variables

When there are two variables like the following we write two variables.



  for x,y st P[x,y] holds Q[x,y]



   proof



    let x,y;



    assume P[x,y];



     ......



     ......



    thus Q[x,y];   (thesis)



   end;

Directly, it means that we demonstrated ( Vx)(Vy)(P(x,y) => Q(x,y)). assume ..... becomes one logical formula.

4.6.2 Method for Writing With such that

In addition, there is another way of writing as follow:



  for x,y st P[x,y] holds Q[x,y]



   proof



    let x,y such that L:P[x,y];



     ......



     ......



     ......



    thus Q[x,y];



   end;

Further, labels are usually entered after such that; however, in this example (this case L) they are not necessary. The first line is st and the third line is such that.

4.6.3 Division of Sentences

There is a skeleton such as this:



  for x,y st P[x,y] & Q[x,y] holds R[x,y]



   proof



    let x,y such that L1:P[x,y] and L2:Q[x,y];



    ......



    ......



    thus R[x,y];



   end;

We can also rewrite this as the following. We need to pay careful attention to the difference of & and and.

The third line



      let x,y such that L1:P[x,y] and L2:Q[x,y];

is



      let x,y such that L:P[x,y] & Q[x,y];

We can also write like the above. Methods for writing the front and back are basically the same. In the method for writing the front, and is used for dividing into two sentences to build other labels. This means that one sentence A & B was divided into sentences A and B. On the other hand, the method for writing the back is persistently one sentence and it is connected by a logical calculation unit. As stated before, we can divide one sentence into two by using and, or, we can connect two sentences into one by using &.

4.6.4 Dividing Sentences With Assume

For the difference in writing a method after such that, a similar thing occurs in the case of assume. For example, adding & S[x,y] to an assume example, we will assume that the following occurred.



  for x,y st P[x,y] & S[x,y] holds Q[x,y]



   proof



    let x,y;



    assume P[x,y] & S[x,y];



    ......



    ......



    thus Q[x,y];



   end;

At this point,



       assume P[x,y] & S[x,y];

can be written as below.



       assume that L1:P[x,y] and L2:S[x,y];

Only with the way of writing the above formula, we can write labels on both P[x,y] and S[x,y]. In this example, they are L1 and L2 labels.

4.6.5 Caution Following that

When using that, we cannot use then after that. It is because we think there may be more than two sentences after such that. When there are more than two sentences, the sentence just before them is not clear.



  assume that A and B;



  then C;

Therefore, the above method of writing is not possible. We have to use labels and write in the following way.



  assume that L1:A and L2:B;



  C by L1,L2;

Or, when only B is used, we can only write as below:



  C by L2;

Also, when there is only one citation, then cannot be used. We have to write by using L2 instead of then. Therefore, when that is stated, labels have to be there or this sentence can not be used. In short, this will not be able to be cited later. Thus, we have to think that there labels will always follow that.

When that is not used, then can be used. Therefore, the first way of writing,

assume P[x,y] & Q[x,y], in this case, the following can be used.



  assume P[x,y] & Q[x,y];



  then ......

Thus, there is only one sentence without that. For assume, then is used.