Rodin User’s Handbook v.2.8: Predicate Logic

2.2.3 Predicate Logic

In predicate logic, statements (which are called predicates) can be expressed with variables that can be quantified (e.g. “for all values of $x$ …”). Event-B uses 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, e.g. 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 value.