User Manual for Rodin v.2.3: Predicate Logic

2.2.3 Predicate Logic

In predicate logic statements (called predicates) can be expressed over variables that can be quantified, like in “for all values of $x$ …”. Event-B’s logic is predicate logic with the following features:

Predicates and expressions are distinguished.
All expressions have a data type, e.g. integer or set of integers.
Quantification over variables, not predicates, is supported. This includes quantification over sets.
A partial function semantics is included, i.e. the predicate $1\div 0 = 1\div 0$ is not a tautology because $1\div 0$ does not represent a valid value.
Comprehension sets are supported.
Predicates can be evaluated to a Boolean values.

Rodin Handbook

2.2.3 Predicate Logic