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.