## 2.8 Put Blocks

When mathematicians define terms and description rules, there are thought
to be four patterns to do so. The first is when the formulas are simply
replaced by some symbols. Thus, when it is written as

"Let's put f(x)=m(x+E) now".

In THEAX, this is called a simple put sentence (grammerically,<simple.put.line>).
For example, the way of writing

a5:Put f(x)=m(Add(x,E));

The second is when functions are defined separately according to the
situations. Therefore, it is when it says

" now, let us put g(x)=0...x it is a rational number, and let
us put g(x)=1...,otherwise".
In THEAX, this is called a compound put sentence(<compound.put.block>).
The way of writing that sentence is:

Put g(x)=;

a8:0 if rational(x);
a9:1 otherwise;
, such that it goes over more than 2 lines.

Third, when there is a y that satisfies certain conditions for each
x and when that is unique, a function that corresponds y for x is defined.
This is similar to a well known Axiom of Choice; however, in the case of
an Axiom of Choice, y does not have to be the only one so this is a weaker
request than an Axiom of Choice. Let us look at an example:

" An element y which satisfies a condition P(x,y), exists uniquely
for every element x in a set G. Consequently, let us put a mapping y=h(x),
which maps an element x in a set G to y." Therefore, if x belongs
to G, P(x,h(x)) holds.
In THEAX, this is called unique put sentence(<unique. put.block>),
and it is written like this:

a5: (All x) (Exist y) (G(x) imp P(x,y)and(All z)((All x)(G(x) imp P(x,z))
imp[z=y])) by......;
When the only existance is demonstrated such as the above, it is written
like below:

Put h; a10 : (All x)(G(x)imp P(x, h(x)));
Well-Defined(a5);
Label a5 of after Well-Defined is pointing to the line that the uniqueness
is demonstrated. Formula a5 can be cited later.

The fourth definition rule is not very popular; however, mathematicians
surely use this logic. For example,

"write one of the roots of X²+1=0 as i, and name it an imaginary
unit".
This is not limited to only one; however, this is to put a name on one
of the things that we know to exists. In the case above, there are i and
-i of roots of X²+1=0; however, it is acceptable to consider -i as
i. This also is not defining an image, so it is different from a choose
axiom. In THEAX, such a definition rule that names existences is called
choose put sentence(<chose.put.block>), and it is written like this:

A1: (Exist x)([Add(Square(x),1)=0]) by ..... ;
When existence of x is demonstrated such as above, it is written like
this:

Put i; B1: [Add(Square(i),1)=0];
Chosen(A1);
A label after Chosen points to the line that asserts existence. The
fact that it is acceptable to quote the line of B1 in later parts is the
same case with a unique put sentence.

At this point, it is unknown why there are four definition rules and
why it is limited to only four. Fewer may be possible if we sort them out
more, or, such as the fourth definition rule, the request might be too
strong. It needs to be further debated.