Chapter 2 Construction of Texts

2.1 Text, End Text

Single mathematics that was written in THEAX language is called text. Text starts with a line of

Text <text name> ;

and finishes with a line of

End Text;

Here, line means letter lines that are sectioned by semicolons (;). <text name> can be chosen from optional names(within 35 letters). Text is constructed by repeating parts of <text block> and that <text block> is either a <axiom block> or a <definition block>. This corresponds to the fact that mathematics is compounded by the repetition of the axiom, theorem, or definition.

(The following part, "Referred" function, has not been achieved in the first version of the checker >>>)

Text fundamentally concludes itself; however, in some cases, it wants to quote the axiom, theory, or definition of other texts. In this case, we insert this special block after the text (in front of other blocks). For instance, when there is a text like figure A, if figure B's text had citation blocks, figure B is considered to be the same kind of text as figure C. Therefore, there is a function that rewrites labels and names according to the direction within the citation blocks. This is helpful to avoid the confusion of symbols when some of the texts get connected. However, this function will be used only after a proper organization is made in the future, registers publicly advertised texts, and opens to the public so that anyone will be able to cite. We hope that in the future, many theories will be stored in the computer and be data based.

Further, real texts are written after putting apostrophes and numbers of every 10 numbers for each line like figures A, B, and C. Many basic texts for personal computers arbitrate this as an annotation line; because of this, we can write optional letter lines and it is useful to utilize personal computers for making THEAX texts.

00010'Text Grasshopper;
00040' A:(All x)(All y)(All z)(Smaller (x,y)and
00050' Smaller(y,z)imp Smaller(x,z));
00060' B:Smaller(Ant,Cricket);
00070' C: Smaller(Cricket,Grasshopper);
00080'End Axiom;
00090'End Text;

Figure A TEXT Grasshopper

00010'Text Mars;Referred;Grasshopper
00020' (L:A to D,Ant to Mars,Cricket to Evening-Glow,
00030 Grasshopper to Wind,Smaller to Higher);
00040'End Refered;
00050'Lemma; A: Higher(Mars,Wind);
00060'Proof; a1:Higher(Mars,Evening-Glow)and Higher(
00070' Evening-Glow,Wind)imp Higher(Mars,Wind) by ALS(D);
00080' a2:Higher(Mars,Wind) by LOGIC(a1,B,C);
00100'End Text;

Figure B Text that cited Grasshopper, Mars

00010'Text Mars;
00040' D:(All x)(All y)(All z)(Higher(x,y)and
00050' Higher(y,z)imp Higher(x,z));
00060' B: Higher(Mars,Evening-Glow);
00070' C: Higher(Evening-Glow,Wind);
00080'End Axiom;
00090'Lemma; A:Higher(Mars,Wind);
00100'Proof; a1:Higher(Mars,Evening-Glow)and Higher(
00110' Evening-Glow,Wind)imp Higher(Mars,Wind) by ALS(D);
00120' a2:Higher(Mars,Wind) by LOGIC(a1,B,C);
00140'End Text;

Figure C Figure B's text can be rewritten like this in a text.