Chapter 1
A Summary of the THEAX Language


1. 1 Concept of Name


Traditionally, mathematics had a writing style that was used habitually by mathematicians; however, it was not strictly established. To input this into computers, (in other words, to make stricter mathematics) we have to determine useful kinds of characters and grammer. Not only grammar, but we have to decide its meaning. This "meaning" is intended for the application of computers at that time; for example, to delete or to register tables of formulas and names. There is this usual question: "Mathematics is said to be the most basic study; however, who can and cannot understand it? Can children or monkeys understand it?" It is also said that the "more we pursue the basic, mathematics becomes progressively complicated". From THEAX's point of view, mathematics is a kind of program. As programs can be understood by both computers and men, mathematics can also be understood by machines and men. It is not that only intellects understand it; if something can distinguish a variety of letters and memorize them and control those operations conditionally and wholeheartedly, it will be fine. On the other hand, children who seem to have great intelligence are not suitable for comprehending mathematics if they are not able to completely control characters. In addition, it is also thought that since basic mathematics, as fundamental program, is not considered to be "exotic" and therefore unable to attract people's interest. Maybe if we ignore practicality, THEAX can come back to its basis. This is possible with formulas and names of simple stuckmachines. Because the structure of that machine can be understood as bits of basic logic by anyone, it is more plain than the turing machine.

THEAX fixes applicable types of characters. It differs in the way that they thought in the past that mathematics can use additional infinite numbers of letters. Mathematicians like special letters that give print shops a hard time. Of course, computers can utilize rare characters such as the APL language; however, assuming that mathematicians of various nationalities do not have the economic power to make computers specifically for mathematics, we want to avoid using special letters that are not needed. For example, logical symbols of V and ] are sufficiently substituted by writing All , Exist. Practicable kinds of letters are capital and small letters of 26 alphabets, numbers, and special symbols /, -, ., +, *, ), (, ;, :, ,, [,]. However, ' is used to indicate the beginning of a text line. There can be other symbols in comments.

THEAX needs the concept of names. Initially, we cannot use any names. After declaring new names by definition and axiom, we are able to use it for the first time. This is similar to the proclamation of used variables of ALGO or PASCAL in computer language. When the names are announced by definition or axiom, THEAX registers these into a table (ntable, a table of names). The length of the names are within 35 letters and are formed by a range of optional alphabets, numbers, and (/, -, .). Names can be variable names or function names.

Examples of names: 1, 0, Nat, Group, Additive-Group, I . Add, Smith85/C23

Furthermore, one needs to pay careful attention since capital and small letters are treated separately (nat and NAT are not the same).

After these names are declared, they are registered to the table mentioned above. Also, during the proof of a definition, temporary names are possible. For example, such contexts as "let's choose optional x from A and fix one," name x is registered to a table temporarily and is treated as though it was proclaimed from the beginning as if it was a proper noun. However, that is transient and names would be deleted from the name table before the proof is finished. In addition, even the contexts such as "let's substitute y for f(x) now," name y is also temporarily registered the same way. Proof is constant repeating of registering and deleting names from a name table.

Names are utilized in the form of a function shown later on. In addition, True and False that indicate logic's truth or false can be managed without declarations like names.