## 1.4 Logical Predicate Formula

THEAX can also manage logical predicate formulas other than logical
preposition formulas. For instance, formulas that include all symbols and
existing symbols are expressed like (~~V~~x) (~~V~~y)
(~~]~~z) f(x, y, z). Here, formulas that follow the quantitized
term (All x)(All y)(Exist z) have to be in parentheses.

For the formula above, it is fine for bounded variables x, y, z to use
other letters. For example, even if we write

(All u)(All v)(Exist w)(f(u,v,w)),
the system can judge that it is the same formula with the one above.
For a bounded variable, same with the letter line of names, we are able
to use within 35 letters of English spellings, numbers, and so on. For
instance, it is acceptable to write:

(All x1)(All x2)(Exist y1-abc)(f(x1,x2,y1-abc))
Further, for this kind of formulas
g(x) and (All x)(f(x)),
a name x(declared or registered) and a restricted variable x are easily
confused. In THEAX, this formula should be interpreted as

g(x) and (All y)(f(y))
however, because the result most likely becomes opposite of what users
intended, it will be wiser to avoid writing in such a manner which can
cause confusion.

Needless to say, quantization can be done repeatedly. Therefore, it
is permitted to write (All x)((All u)(f(x,u)imp(Exist z)(g(x,u,z))and q(x)).