# 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.

- Concerning propositional logic ...LOGIC
- Concerning predicate logic ........ALS, EXIST, ALIM, EXIM, ARRN, FLW,
ORD, DMOR, CNST, (FUNF)
- Concerning equation .................EQ, (EQPT)
- Concerning substitution..............SUBST, EQPT, FUNF

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.