Chapter 3 Inference Rule


3.1 The Outline of the Inference Rule


There are 14 inference rules ready in THEAX (in Ver.1.0). We roughly divide and indicate them as follows.

If we look at it this way, the most numerous concern predicate logic . FUNF and EQPT are inference rules that were compounded. Therefore, we can precede with the definition without them for the time being. However, we would be able to have a simple description if we had them. In addition, ORD, DMOR, CNST, and EQ are not necessary; however, it would be convenient if they existed. Thus, inference rules are not chosen from absolute necessity, but it is chosen with the main purpose of formulating the things that were used traditionally by mathematicians consciously or unconsciously. It is because our goal is to provide a practical language for mathematical description as much as it is possible. (However, at the same time, we want to make a certain impact on basic mathematical theory...) As revisions of THEAX progresses (improvement of Version), there are possibilities of using more inference rules, or on the other hand, it is possible that we would be exclusively limited to basically one rule. To explain the latter in an extreme example, when computers execute the rules above, it is fine if the OK sign appears among one of the 14 rules. Therefore, it is possible to only write "from formulas 1 and 2," like traditional mathematics dictates.