1.2. Introduction to predicate logic¶

This section provides a basic introduction to predicates, propositional logic and quantifiers. These basic concepts of mathematical logic are useful when doing formal verification, and in particular when working with the Prover. If you are familiar with these concepts, feel free to skip this section. If you wish to test your knowledge, use the Quiz below.

Propositional logic¶

Propositional logic is the basis of mathematical logic, dealing with boolean variables and operations.

Propositions¶

We can think of a proposition as a function where:

all inputs have type bool
the return type is also bool
only logical operators are allowed in the body of the function

Example:¶

Consider the proposition \(P\) which is “\(Q\) and \(R\)”. In mathematical notation this is \(P = Q \land R\), and in CVL we can write it as:

function P(bool Q, bool R) returns bool {
    return Q && R;
}

More informally, we can simply write this proposition as a boolean expression:

bool P = Q && R;

Note

The definition for a proposition given here is not the classical one. However, it is equivalent and easier to explain in our context.

The implication operator¶

In propositional logic, the statement \(P\) implies \(Q\) means that if \(P\) is true then \(Q\) is also true. Hence the statement is true when either both \(P\) and \(Q\) are true, or when \(P\) is false. A complete truth table is given below in Example: Implication truth table.

In mathematical notation the statement is \(P \implies Q\), and in CVL the syntax is P => Q.

Examples¶

Here are some more examples, shown in mathematical notation and in CVL side by side.

Math

\((Q \vee R) \implies (P \land S)\)

CVL

(Q || R) => (P && S)

Math

\((P \implies (Q \vee R)) \land (\neg P \implies S)\)

CVL

(P => (Q || R)) && (!P => S)

Truth tables¶

Since the variables of a proposition are all boolean, we can enumerate them in a table and find the output for every set of inputs. This is known as a truth table.

Example: Implication truth table¶

Here is the truth table for the proposition \(A\) defined as “\(B\) implies \(C\)”. In mathematical notation this is \(A = \left( B \implies C \right)\) and in CVL:

bool A = B => C;.

Truth table for implication¶
B	C	A
false	false	true
false	true	true
true	false	false
true	true	true

The truth table describes the action of the implication operator \(\implies\).

Predicates¶

We can think of a predicate as a function whose return type is bool, i.e. returns either true or false.

Example:¶

The function “is \(n\) divisible by 3” is a predicate. Here is the function in mathematical notation:

\begin{equation} f: \mathbb{N} \to \{ \text{true, false} \}, \quad f(n) = \begin{cases} \text{true} & \text{if } n \vert 3 \\ \text{false} & \text{otherwise} \end{cases} \end{equation}

In CVL it looks like this:¶

function f(int n) returns bool {
    return 3 * (n / 3) == n;
}

Quantifiers¶

The statement “there exists a natural number \(n\) which is divisible by 3” is an example of a quantifier. This statement is true, since \(n=3\) is indeed divisible by 3. In general, given a predicate \(f(x)\) where \(x\) belongs to some set \(S\), we can use a quantifier on \(f\) to make a statement in one of two ways.

Exists¶

We can claim “there exists \(x \in S\) such that \(f(x)\) holds”. This is the exists quantifier, denoted \(\exists\). In mathematical notation this statement is:

\[\exists x \in S. f(x)\]

The exists quantifier can be thought of as a using the or operator over all \(x \in S\). For example, the statement “there exists a natural number \(n\) which is divisible by 3” is the same as:

\[(1 \vert 3) \vee (2 \vert 3) \vee (3 \vert 3) \vee (4 \vert 3) \cdots = \bigvee_{n \in \mathbb{N}} n \vert 3\]

Solidity code realizing this is:

function existsDivisibleByThree() external returns (bool) {
  for (uint256 i = 1; i < type(uint256).max; i++) {
    if (i % 3 == 0) return true;
  }
  return false;
}

In CVL we have the keyword exists, for example:

require (exists uint n. (n % 3) == 0);

For all¶

The forall quantifier requires that the predicate be satisfied by all possible inputs. An example of this is the statement: “for all natural numbers \(n\) either \(n\) is even, or \(n + 1\) is even”. The forall quantifier is denoted \(\forall\), so the statement in mathematical notation is:

\[\forall n \in \mathbb{N}. (n \vert 2) \vee (n + 1 \vert 2)\]

In general, given a predicate \(f(x)\) where \(x \in S\), we can form the statement \(\forall x \in S. f(x)\). The forall quantifier is the same as using the and operator on \(f(x)\) for all \(x \in S\), in mathematical notation:

\[\forall x \in S. f(x) = \bigwedge_{x \in S} f(x)\]

The negation of a forall statement can be given in the form of an exists statement, like this (the negation is denoted by the symbol \(\neg\)):

\[\neg \left( \forall x \in S. f(x) \right) = \exists x \in S. \neg f(x)\]

This comes in handy when writing code realizing a forall statement.

Example:¶

Here is the solidity code realizing the statement “for all \(n\) either \(n\) is even, or \(n + 1\) is even”:

function allAreEven() external returns (bool) {
  for (uint256 i = 1; i < type(uint256).max; i++) {
    if (i % 2 != 0 && (i + 1) %2 != 0) return false;
  }
  return true;
}

In CVL we have the keyword forall, for example:

require (forall uint n. (n % 2 == 0) || ((n + 1) % 2 == 0));

Vacuity¶

Consider the statement: “For all \(n \in \mathbb{N}\) if both \(n\) and \(n + 1\) are even, then \(n = n + 2\) “. In mathematical notation:

\[\forall n \in \mathbb{N}. (n \vert 2) \land (n + 1 \vert 2) \implies (n = n + 2)\]

Surprisingly, this statement is true. Because for every \(n\) the part \((n \vert 2) \land (n + 1 \vert 2)\) is always false, so by the Truth table for implication the implication is true.

In general, given a statement of the form \(\forall x \in S. f(x) \implies g(x)\) where \(f\) and \(g\) are predicates, we say the statement holds vacuously (or is satisfied vacuously) if \(\forall x \in S. \neg f(x)\). This means there is not even a single element \(x \in S\) for which \(f(x)\) holds.

While this may seem like an edge case, it can easily occur that heaping conditions on a statement ends with the statement being satisfied vacuously.

Logical operators and quantifiers¶

Logical operators and quantifiers table¶
Name	Math symbol	CVL	Description
and	\(\land\)	`&&`	And operation
or	\(\vee\)	`\|\|`	Or operation
implies	\(\implies\)	`=>`	Implication operation
not	\(\neg\)	`!`	Negation operation
if and only if	\(\Longleftrightarrow\)	`<=>` (also `==`, see below)	Equality of booleans
forall	\(\forall\)	`forall`	For all elements in a set, it holds that …
exist	\(\exists\)	`exist`	There exists an element in a set, such that …

Note

The “if and only if” operator is the same as euqality of booleans, meaning \(P \Longleftrightarrow Q\) is the same as P == Q.

Quiz¶

Test your knowledge with our quiz below (additional questions can be found on the first part of the Secureum Quiz).

When is the expression \(P \implies Q\) false?
1. When \(\neg P \land \neg Q\) is true (i.e. when both \(P\) and \(Q\) are false)
2. When \(P \land Q\) is true
3. When \(\neg P \land Q\) is true
4. None of the above
When is the expression \(P \land Q \ \implies P\) true?
1. Always (it is true in all cases)
2. Never (it is false in all cases)
3. True for some cases and false for others
4. None of the above
When is the expression \(\left( P \land \left( Q \vee \neg P \right) \right) \land \neg Q\) true?
1. Always (it is true in all cases)
2. Never (it is false in all cases)
3. True for some cases and false for others
If we know that the expression \(P \implies \left(P \land \neg Q \right)\) is true, and that \(P\) is true, then we can deduce that:
1. \(Q\) is true
2. \(Q\) is false
3. \(Q\) can be either true or false (we can deduce nothing)