Peano's axiom is famous for the natural number theory. However, it is not certain if that axiom system is enough. In reality, when opening up the theory for the natural numbers, it is difficult to decide how to bring in the functions that will be inductively defined like the factorial function n!. Since it is a definition of the inductive function, the axiom concerning the inductive method seems enough. However, let us carefully look at the following examples of the definition of the factorial functions.

1 ! = 1

assuming until n ! is defined

(n + 1) ! = (n + 1) ~ n !

With this, all nutural numbers k, k! can be defined.

In addition, to recall what the inductive method is,

P (1) is formed

if P (n) is formed,

P (n + 1) is also formed

Then, all nutural numbers k, P(k) will be formed.

These are very similar. If we state P(x)="x! can be defined", it seems as though the inductive function can be defined through the inductive method. However, when we think this over, definable or not is the problem former to the axiom. That should not be selfishly decided within the theory. Similar to the way of writing an axiom, the definition method became independent from each theory. If inductive definition is permitted, it means that the definition method using the natural number concept is given former to the axiom of the natural numbers, it would become preposterous.

Even when it is impossible to place the proposition saying "x! can be defined", we wonder if there is any other way to define n!. The following view point can be stated: the reason why the inductive method can not be used directly is because the inductive method can not insure the "existence of the functions". The inductive method insures the formation of the propositions against each natural number; however, it is impossible to insure the functions' existence because they are separated from each natural number, meaning that they are more advanced concepts. Therefore, isn't following an axiom necessary for one of the axioms of the natural numbers?

The function f that satisfies the next two conditions (natural numbers as the definition limit) exists.

Here, a can be optional and b is a function that has an appropriate definition limit and two variables. If the existence of the function f can be indicated according to the conditions above, then it is possible to name f by the choose put sentences. Further, f looks to be fixed solely in number 1 and 2; however, because THEAX does not restrict the functions' definition limit, it means that the values other than the natural numbers have options. That is why f is not unique. Therefore, one of those is named by the choose put sentences such as "Fac" (abbreviation of factorial).

The conditions above becomes the following formula.

Our proposal is to add this to the axiom as a label Nat 10 with a name "axiom of the inductive function." However, a better way of defining, for example, factorial functions maybe possible. We are looking forward to hearing the opinions of the readers.