This work is sponsored by the
Deploy Project
This work is sponsored by the
ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
Predicates
Rodin User’s Handbook v.2.8
 



Rodin User’s Handbook v.2.8 



3.3.2 Predicates
3.3.2.1 Logical primitives

true 
True 

false 
False 
 Description
The predicates and are the predicates that are true and false respectively.
 WD
3.3.2.2 Logical operators

& 
Conjunction 

or 
Disjunction 

=> 
Implication 

<=> 
Equivalence 

not 
Negation 
 Description
These are the usual logical operators.
 Definition
The following truth tables describe the behaviours of these operators:
 Types
All arguments are predicates.
 WD
Please note that the operators and are not commutative because their welldefinedness conditions distinguish between the first and second argument. Therefore, if their arguments have welldefinedness conditions, the order matters. For example, is always welldefined, but still has the welldefinedness condition .
3.3.2.3 Quantified predicates

! 
Universal quantification 

# 
Existential quantification 
 Description
The universal quantification is true if is satisfied for all possible values of . A usual pattern for quantification is where is used to specify the types of the identifiers. The existential quantification is true if a value of exists such that is satisfied. The types of all identifiers must be inferable by . They can be referenced in .
 Types
The quantifiers and the are predicates.
 WD
3.3.2.4 Equality

= 
equality 

/= 
inequality 
 Description
Checks if both expressions are or are not equal.
 Definition
 Types
and are predicates with and , i.e. and must have the same type.
 WD
3.3.2.5 Membership

: 
set membership 

/: 
negated set membership 
 Description
Checks if an expression denotes an element of a set .
 Definition
 Types
and are predicates with and .
 WD
