Rodin Handbook





 

3.3.2 Predicates

3.3.2.1 Logical primitives

$\mathord {\top }$

true

True

$\mathord {\bot }$

false

False

Description

The predicates $\mathord {\top }$ and $\mathord {\bot }$ are the predicates that are true and false respectively.

WD

$\mathcal{L}(\mathord {\top }) \mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\mathord {\bot }) \mathrel {\widehat=}\mathord {\top }$


3.3.2.2 Logical operators

$\land $

&

Conjunction

$\lor $

or

Disjunction

$\mathbin \Rightarrow $

=>

Implication

$\mathbin \Leftrightarrow $

<=>

Equivalence

$\lnot $

not

Negation

Description

These are the usual logical operators.

Definition

The following truth tables describe the behaviours of these operators:

$\textsf{P}$

$\textsf{Q}$

$\textsf{P}\land \textsf{Q}$

$\textsf{P}\lor \textsf{Q}$

$\textsf{P}\mathbin \Rightarrow \textsf{Q}$

$\textsf{P}\mathbin \Leftrightarrow \textsf{Q}$

$\mathord {\bot }$

$\mathord {\bot }$

$\mathord {\bot }$

$\mathord {\bot }$

$\mathord {\top }$

$\mathord {\top }$

$\mathord {\bot }$

$\mathord {\top }$

$\mathord {\bot }$

$\mathord {\top }$

$\mathord {\top }$

$\mathord {\bot }$

$\mathord {\top }$

$\mathord {\bot }$

$\mathord {\bot }$

$\mathord {\top }$

$\mathord {\bot }$

$\mathord {\bot }$

$\mathord {\top }$

$\mathord {\top }$

$\mathord {\top }$

$\mathord {\top }$

$\mathord {\top }$

$\mathord {\top }$

$\textsf{P}$

$\lnot \textsf{P}$

$\mathord {\bot }$

$\mathord {\top }$

$\mathord {\top }$

$\mathord {\bot }$

Types

All arguments are predicates.

WD

Please note that the operators $\land $ and $\lor $ 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, $x\neq 0 \land y\div x=3$ is always well-defined, but $y\div x=3 \land x\neq 0$ still has the well-definedness condition $x\neq 0$.

$\mathcal{L}(\textsf{P}\land \textsf{Q}) \mathrel {\widehat=}\mathcal{L}(\textsf{P}) \land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{Q}))$
$\mathcal{L}(\textsf{P}\lor \textsf{Q}) \mathrel {\widehat=}\mathcal{L}(\textsf{P}) \land (\textsf{P}\lor \mathcal{L}(\textsf{Q}))$
$\mathcal{L}(\textsf{P}\mathbin \Rightarrow \textsf{Q}) \mathrel {\widehat=}\mathcal{L}(\textsf{P}) \land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{Q}))$
$\mathcal{L}(\textsf{P}\mathbin \Leftrightarrow \textsf{Q}) \mathrel {\widehat=}\mathcal{L}(\textsf{P}) \land \mathcal{L}(\textsf{Q})$
$\mathcal{L}(\lnot (\textsf{P})) \mathrel {\widehat=}\mathcal{L}(\textsf{P})$


3.3.2.3 Quantified predicates

$\forall $

!

Universal quantification

$\exists $

#

Existential quantification

Description

The universal quantification $\forall x_1,\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}$ is true if $\textsf{P}$ is satisfied for all possible values of $x_1\ldots ,x_ n$. A usual pattern for quantification is $\forall x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}_1\mathbin \Rightarrow \textsf{P}_2$ where $\textsf{P}_1$ is used to specify the types of the identifiers.

The existential quantification $\exists x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}$ is true if a value of $x_1\ldots ,x_ n$ exists such that $\textsf{P}$ is satisfied.

The types of all identifiers $x_1\ldots ,x_ n$ must be inferable by $\textsf{P}$. They can be referenced in $\textsf{P}$.

Types

The quantifiers and the $\textsf{P}$ are predicates.

WD

$\mathcal{L}(\forall x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}) \mathrel {\widehat=}~ \forall x_1\ldots ,x_ n \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P})$
$\mathcal{L}(\exists x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}) \mathrel {\widehat=}~ \forall x_1\ldots ,x_ n \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P})$


3.3.2.4 Equality

$=$

=

equality

$\neq $

/=

inequality

Description

Checks if both expressions are or are not equal.

Definition

$\textsf{E}\neq \textsf{F}\mathrel {\widehat=}\lnot ( \textsf{E}=\textsf{F})$

Types

$\textsf{E}= \textsf{F}$ and $\textsf{E}\neq \textsf{F}$ are predicates with $\textsf{E}\in \alpha $ and $\textsf{F}\in \alpha $, i.e. $\textsf{E}$ and $\textsf{F}$ must have the same type.

WD

$\mathcal{L}(\textsf{E}= \textsf{F}) \mathrel {\widehat=}\mathcal{L}(\textsf{E}) \land \mathcal{L}(\textsf{F})$
$\mathcal{L}(\textsf{E}\neq \textsf{F}) \mathrel {\widehat=}\mathcal{L}(\textsf{E}) \land \mathcal{L}(\textsf{F})$


3.3.2.5 Membership

$\in $

:

set membership

$\not\in $

/:

negated set membership

Description

Checks if an expression $\textsf{E}$ denotes an element of a set $\textsf{S}$.

Definition

$\textsf{E}\not\in \textsf{S}\mathrel {\widehat=}\lnot (\textsf{E}\in \textsf{S})$

Types

$\textsf{E}\in \textsf{S}$ and $\textsf{E}\not\in \textsf{S}$ are predicates with $\textsf{E}\in \alpha $ and $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$.

WD

$\mathcal{L}(\textsf{E}\in \textsf{S}) \mathrel {\widehat=}\mathcal{L}(\textsf{E}) \land \mathcal{L}(\textsf{S})$
$\mathcal{L}(\textsf{E}\not\in \textsf{S}) \mathrel {\widehat=}\mathcal{L}(\textsf{E}) \land \mathcal{L}(\textsf{S})$