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 (Vx) (Vy) (]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)).