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.
See also
You can find further information about these subjects in:
Chapter 1 of Introduction to Logic (written by Patrick Suppes)
Chapter 3.1 of Discrete Mathematics  An Open Introduction
Tip
At the end of this section there is a handy table containing the common symbols for the logical operators and quantifiers introduced here. See Logical operators and quantifiers table.
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.
\((Q \vee R) \implies (P \land S)\)
(Q  R) => (P && S)
\((P \implies (Q \vee R)) \land (\neg P \implies S)\)
(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;
.
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:
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:
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:
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:
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:
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\)):
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:
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¶
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\) 

Equality of booleans 
forall 
\(\forall\) 

For all elements in a set, it holds that … 
exist 
\(\exists\) 

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?
When \(\neg P \land \neg Q\) is true (i.e. when both \(P\) and \(Q\) are false)
When \(P \land Q\) is true
When \(\neg P \land Q\) is true
None of the above
When is the expression \(P \land Q \ \implies P\) true?
Always (it is true in all cases)
Never (it is false in all cases)
True for some cases and false for others
None of the above
When is the expression \(\left( P \land \left( Q \vee \neg P \right) \right) \land \neg Q\) true?
Always (it is true in all cases)
Never (it is false in all cases)
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:
\(Q\) is true
\(Q\) is false
\(Q\) can be either true or false (we can deduce nothing)