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
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
In mathematical notation the statement is P => Q
.
Examples¶
Here are some more examples, shown in mathematical notation and in CVL side by side.
(Q || R) => (P && 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
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
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
function f(int n) returns bool {
return 3 * (n / 3) == n;
}
Quantifiers¶
The statement
“there exists a natural number
Exists¶
We can claim “there exists
The exists quantifier can be thought of as a using the or operator over all
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
In general, given a predicate
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
This comes in handy when writing code realizing a forall statement.
Example:¶
Here is the solidity code realizing the statement “for all
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
Surprisingly, this statement is true. Because for every
In general, given a statement of the form
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 |
|
And operation |
|
or |
|
Or operation |
|
implies |
|
Implication operation |
|
not |
|
Negation operation |
|
if and only if |
|
Equality of booleans |
|
forall |
|
For all elements in a set, it holds that … |
|
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 == 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
false?When
is true (i.e. when both and are false)When
is trueWhen
is trueNone of the above
When is the expression
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
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
is true, and that is true, then we can deduce that: is true is false can be either true or false (we can deduce nothing)