4.7 Existing Symbols

There are more different kinds of skeletons. In the case of demonstrating logical predicate formulas with existing symbols ex x st P[x], we use take.

By using take, we write the following:



  ex x st P[x]



   proof



    L:P[a];



    take x=a;



    then P[x] by L;



    thus thesis;



   end;

When demonstrating the existence of x that satisfies P[x], let us assume that P[a] is demonstrated. In this case, it means that for take x=a, x is exists and if we take a, it is demonstrated by L.

4.7.1 Method for Using Consider

Consider is an opposite word for take.



  (ex x st P[x]) implies for y st Q[y] holds R[y]



   proof



    assume ex x st P[x];



    then consider a such that L:P[a]



    ......



    ......



    let y such that Q[y];



    ......



    ......



    thus R[y];



   end;

First, we will assume. For assume ex x st P[x];, we use consider and state then consider a such that L:P[a]. This case also needs labels because such that exists. We will leave it like this and to state y st next, we will state let y such that Q[y] to state thus Q[y].

Consider means to give some sort of proper nouns to an existing x that satisfies P[x]. Therefore, we intend to have an existing x as a topic for discussion. Thus, it does not have to be x, it can be a.

As an existing a, it can be used as a proper noun here. In other words, it is used as if it is assumed to exist. Therefore, consider is an opposite of take. Take is used for replacing something as a proper noun or bring in existing symbols.

4.7.2 Method for Using Given

There is another skeleton that is slightly different.



  (ex x st P[x]) implies for y st Q[y] holds R[y]



   proof



    given x such that P[x];



    ......



    ......



    let y



    assume Q[y];



    ......



    ......



    thus R[y];



   end;

Here, please remember that given in the second sentence, given x such that P[x] ;, works as both assume and consider. It is much easier.