2.11 Unique Put Sentences

In traditional mathematics, such sentences as "corresponding with original x of optional set A, only y that satisfies a proposition f(x,y) exists. Therefore, let us put an image g(x) that corresponds y with original x of A". In THEAX, this is written as following.

Put g :
Ab 10 : (All x)(A(x) imp f(x, g(x))) ; Well-Defined (Ab7) ;

In here, Ab10 and Ab7 are labels. Following Well - Defined, Ab7 is a formula as below. This emphasizes the uniqueness of an origin that corresponds with x and that formation has to be indicated before this unique put sentence.

Ab7 : (All x)(A(x) imp (Exist y)(f(x,y) and (All u)(f(x,u) imp [u=y])))

Thus, this expresses that y exists and if u also satisfies f(x,u), it has to be u=y.

Figure A shows the definition of optional join U of a half group. The (2) defines an image Joi(x,y) of a set x,y as the minimum ceiling of the set constructed from 2 points, Set2(x,y)={x,y}. The (1)is an expression of that uniqueness.

Figure B is a definition of an image unit (G,p) that corresponds optional group G (and its proposition p) with its original unit (this is definable once at least and in reality, it is not used often). It is because mathematicians usually do not consider such as sets of all groups. However, unity of a group G is often indicated with such letters as e. In that case, because the e does not indicate the unity of a specific group, it is not a pronoun. If a group G changes to something else, e also has to change. In that sense, we can think that e is also working imaginatively like the unit above.

Here, we will indicate the general way of writing unique put sentences.

Put<name>;<label>:(All <name>) (All <name>)....<logic.pre.formula>imp <term>);
Well-Defined (<label>);

Also, the formulas that show their uniqueness take the following form.

<label>: (All <name>) (All <name>)...<logic. pre. formula>imp (Exist <name>) (<term>and (All <name>) (<term>imp [<name>=<name>])));

00630 'Lemma;/* x join y is unique */

00640 ' PosLem1: (All x)(All y)(Jsl(x)and Jsl(y)imp

00650 ' (Exist z)(l.u.b.(osL)(Set2(x,y))(z)

00660 ' and (All u)(l.u.b.(osL)(Set2(x,y))(u)

00670 ' imp [u=z])));


00960 'Definition;/* Join operation*/

00970 ' Put Joi; PosDe6:(All x)(All y)(Jsl(x)and Jsl(y)

00980 ' imp l.u.b.(osl)(Set2(x,y))(Joi(x,y))) ;

00990 ' Well-Defined(PosLem1) ;

01000 'End Def ;

(2) Figure A Definition of an image that corresponds to a set x and y with the join x U y.

00570 'Proposition;/* Uniqueness of Left Unity */

00580 ' GrPro4: (All G)(All P)(Group(G,P)imp(Exist i)(G(i)and

00590 ' (All x)(G(x)imp[P(i,x)=x])and(All u)(G(u)and(All x)

00600 ' (G(x)imp[P(u,x)=x])imp[u=i])));


01290 'Definition;Put unit;GrDe2:(All G)(All P)(Group(G,P)imp

01300 ' G(unit(G,P))and (All x)(G(x)imp[P(unit(G,P),x)=x]));

01310 ' Wll-Defined(GrPro4);

01320 'End Def;

(2) Figure B Definition of an image that corresponds the optional group (G, p) with its original unit.