|
true |
True |
|
false |
False |
The predicates and
are the predicates that are true and false respectively.
|
& |
Conjunction |
|
or |
Disjunction |
|
=> |
Implication |
|
<=> |
Equivalence |
|
not |
Negation |
These are the usual logical operators.
The following truth tables describe the behaviours of these operators:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
All arguments are predicates.
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
.
|
! |
Universal quantification |
|
# |
Existential quantification |
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
.
The quantifiers and the are predicates.
|
= |
equality |
|
/= |
inequality |
Checks if both expressions are or are not equal.
and
are predicates with
and
, i.e.
and
must have the same type.
|
: |
set membership |
|
/: |
negated set membership |
Checks if an expression denotes an element of a set
.
and
are predicates with
and
.