The quantifier functions represent logical assertions.  They always return in unevaluated form, subject to basic type checks, variable-binding checks, and some canonicalization.

The quantifier functions do not attempt to evaluate truth values of given assertions, nor do they mandate any assumptions or constraints on any "variables" in the Maple session; rather, they act as placeholders to represent assertions for interpretation by other applications.

The arguments to a quantifier call are subject to the usual Maple evaluation of function arguments.

The predicate need not be of Maple type boolean, which allows the use of expressions such as P(x), P(true), P, or another quantifier.  Symbolic constants are not allowed with the exception of 'true' or 'false'.

Quantifiers can be nested by using a quantifier as (or as part of) the predicate of an enclosing quantifier.  The bound variable of the enclosing quantifier will often be the same as a parameter (or free variable) of an inner quantifier.  Thus, the formerly free variable of the inner quantifier has been bound at an outer level.

If in a quantifier call, the bound variable is already bound in another quantifier enclosed in the predicate, an error is returned.

A normalized quantifier always has the bound variable(s) in a single argument (a name or list of names) and the predicate as the second argument.

If a quantifier function is called with more than two arguments (such as quant( arg1, arg2, arg3, ... )), a quantifier function with bound variable arg1 and predicate as another quantifier of the same kind of the remaining arguments (such as quant( arg1, quant( arg2, arg3, ...) )) is returned. In other words, a recursive nesting of quantifiers is attempted, with an innermost quantifier of the last two original arguments.  This will return an error if the resulting  bound variables are not distinct.

A quantifier function can be called with a list of bound variables, which will be preserved as such in the returned object.  Maple considers this form to be logically equivalent to a recursively nested form (see above), where the first element of the bound variable list is bound at the outermost level, and the last element is bound at the innermost level.  An error is returned if the bound variables in the list are not distinct.  If an empty list is specified, the predicate is simply returned (if valid).

No further simplifications are performed based on any interpretation of the quantifier, regardless of the state of the rest of the Maple session.  For example, even with the case of a trivial predicate as in forall(x,true), the quantifier is not "simplified" to 'true'.

Although a quantifier can formally be interpreted as having a Boolean value, it is not of Maple type boolean.

If, in the predicate of a quantifier, the bound variable were replaced with any particular value from its anticipated universe (which is not explicitly specified), the predicate should either evaluate to a Boolean constant or have the potential to do so, or at least be formally interpreted as Boolean.

Error, (in exists) y already bound in predicate