User Manual for Rodin v.2.3: Predicates

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 give an overview:

$P$	$Q$	$P\land Q$	$P\lor Q$	$P\mathbin \Rightarrow Q$	$P\mathbin \Leftrightarrow 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 }$

$P$	$\lnot 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. E.g. $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}(P\land Q) \mathrel {\widehat=}\mathcal{L}(P) \land (P \mathbin \Rightarrow \mathcal{L}(Q))$
$\mathcal{L}(P\lor Q) \mathrel {\widehat=}\mathcal{L}(P) \land (P \lor \mathcal{L}(Q))$
$\mathcal{L}(P\mathbin \Rightarrow Q) \mathrel {\widehat=}\mathcal{L}(P) \land (P \mathbin \Rightarrow \mathcal{L}(Q))$
$\mathcal{L}(P\mathbin \Leftrightarrow Q) \mathrel {\widehat=}\mathcal{L}(P) \land \mathcal{L}(Q)$
$\mathcal{L}(\lnot (P)) \mathrel {\widehat=}\mathcal{L}(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}~ P$ is true if $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}~ P_1\mathbin \Rightarrow P_2$ where $P_1$ is used to specify the types of the identifiers.

The existantial quantification $\forall x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P$ is true if there is a valuation of $x_1\ldots ,x_ n$ such that $P$ is satisfied.

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

Types

The quantifiers and the $P$ are predicates.

WD

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

3.3.2.4 Equality

$=$	`=`	equality
$\neq$	`/=`	inequality

Description: Checks if both expressions are (not) equal.
Definition: $E \neq F \mathrel {\widehat=}\lnot ( E=F)$
Types: $E = F$ and $E \neq F$ are predicates with $E\in \alpha$ and $F\in \alpha$ , i.e. $E$ and $F$ must have the same type.
WD: $\mathcal{L}(E = F) \mathrel {\widehat=}\mathcal{L}(E) \land \mathcal{L}(F)$
$\mathcal{L}(E \neq F) \mathrel {\widehat=}\mathcal{L}(E) \land \mathcal{L}(F)$

3.3.2.5 Membership

$\in$	`:`	set membership
$\not\in$	`/:`	negated set membership

Description: Checks if an expression $e$ denotes an element of a set $S$ .
Definition: $e \not\in S \mathrel {\widehat=}\lnot ( e\in S)$
Types: $e \in S$ and $e\not\in S$ are predicates with $e\in \alpha$ and $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ .
WD: $\mathcal{L}(e\in S) \mathrel {\widehat=}\mathcal{L}(e) \land \mathcal{L}(S)$
$\mathcal{L}(e\not\in S) \mathrel {\widehat=}\mathcal{L}(e) \land \mathcal{L}(S)$

Rodin Handbook