1.2 General Function Form


Traditionally, such expressions as f(x) were not clear if it meant the value of x or the function itself. In THEAX, f(x) indicates the value of the function. A function is simply stated only with f. Then there would be a question of how one knows that f is not plainly a variable but a function. In fact, the THEAX system does not concern itself with f being a function or a variable. Therefore, it is not wrong to merely write f or think f as 2 variables and write f(x,y). However, in reality, because f is treated as one variable so that a form f(x, y) does not appear during the definition or axiom, the proof of a proposition for f(x, y) cannot be much.

THEAX can also express a functional other than function. This can be done by writing such as g(x) (y). This means that when one x is fixed, a single function in respect to y is set. g(x) expresses a function that makes y a variable and g(x) (y) indicates the value of that function for y. Strictly, g indicates a functional (a function that values a function). Also, more complicated expression such as h (x, y) (u, v) (z) can be permitted. This is the statement of a function that values a functional.

Moreover, THEAX does not distinguish between a function and a predicate proposition. A predicate proposition concludes that it is a function that values True or False. Therefore, first and high orderedpredicate logic are managed without differentiation. For example, substituting all symbols for All, if there is a predication such as

(All x) (x (s))

at this point, it is possible to draw out f (s) or g(c) (s) and h(n, m) (i, j) (s). Also, from (All y) (y(s,t) (u)) one can derive h(n,m) (s,t) (u).