## 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 well-definedness conditions distinguish between the first and second argument. Therefore, if their arguments have well-definedness conditions, the order matters. For example, is always well-defined, but still has the well-definedness 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