The usual first-order quantification and logical connectives are provided.Many algebraic specification frameworks allow quantifiers and the usual logical connectives: the adjective `algebraic' refers to the specification of algebras, not to a possible restriction to purely equational specifications, which are algebraic in a different sense. But of course many prototyping systems do restrict specifications to (conditional) equations, so as to be able to use term rewriting techniques in tools; this will be reflected in restrictions of CASL to sublanguages.
Predicates for use in atomic formulae may be declared.It is quite common practice to eschew the use of predicates, taking (total) functions with results in some built-in sort of Boolean truth-values instead. As with restrictions to conditional equations, this may be convenient for prototyping, but it seems difficult to motivate at the level of using CASL for general specification and verification.
The crucial argument, however, for allowing predicates instead of requiring the use of truth-valued functions, is that the former allow inductive specifications of relations, e.g., transitive closure.
Hence predicates may be declared, and combined using the standard logical connectives.