We often use this sentence: "there is at least one x that satisfies P(x). Let us give a name for one of these". Therefore, selecting one of the existences arbitrally and name it. This is different from a unique put sentences in a way that it only defines names instead of images. With the same reason, it is also different from what is called axiom of choice.
Here, labels of formulas after Chosen indicate the existence of x as following.
AC7 : (Exist x) (P(x)) ;
The formula AC 10 is formed by replacing the restricted variable x by the existence symbols of AC7 with a new name a and excluding the existence symbols.
Furthermore, when deleting the existence symbols from the formula AC7, one pair of parentheses in both sides of of P(x) are also deleted. Therefore, in case of the formula AC7 is as follows,
(Exist x) (All y) (P (x,y)) ;
we have to transform this into a formula with more parentheses like below.
(Exist x) ((All y) (P (x,y))) ;
Chosen put sentences are not used in the theorem demonstrations. It is because if we utilize quantitization blocks like the following, it will work in the same way with chosen put sentences.
Therefore, one can say that chosen put sentences are applied when he/she wants to use the result of quantitization blocks within the largely limited logics outside the demonstrations. However, it needs more discussion later on because it is not substituting every function of the quantitization blocks.
Figure A shows an example of using the chosen put sentences for the factorial definition. We do not know if this example is an appropriate one because it is related to the factorial function that was traditionally possible to define only by mathematical induction. For instance,
We often see such a way of writing as above. However, mathematical induction is a concept that is guranteed by the axiom of natural numbers. It is questionable to restrict the definition method with its axiom being the frame of mathematics. In addition, normal mathematical induction in reality does not state the defintion method. In spite of that, it seems improper to justify such a logic as above. Accordingly, figure A tried the definition of factorial functions by applying chosen put sentences ( also in the case of using this definition, one more axiom needs to be added to the system of natural numbers. More details are shown in the system of natural numbers at the end of this book).
In addition, chosen put sentences' proper form of the writing method is shown below.
Here, formulas that are indicated by the label after Chosen take the following form.
10450 'Proposition; NaProA:(Exist f)([f(1)=1]and
10460 ' (All n)(Nat(n)imp[f(Pl(n))=Prd(Pl(n),f(n))]));
10580 'Definition;/*Def of n! */
10590 ' Put Fac; NaDeB: [Fac(1)=1]and(All n)(Nat(n)imp
10600 ' [Fac(Pl(n))=Prd(Pl(n),Fac(n))]);
10610 ' Chosen (NaProA);
Figure A An example using chosen put sentences for the definition of factorial !