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

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: