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
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:
a name x(declared or registered) and a restricted variable x are easily confused. In THEAX, this formula should be interpreted as
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)).