Definitions
Predicates
For the moment, with our language we do not have the possibility of
reasoning about objects like, for example, natural or integer numbers.
Furthermore, we would like to be able to express properties on such objects
or relations between them, thus we would like to have the so-called
predicates. For example, a property of an integer number is
that of being prime: 5 is prime.
An example of relation between numbers is the fact that a number is greater
than another one: 5 is greater than 3.
We add the possibility of having predicates in our formal language
using an applicative notation:
- (Prime 5) represents the fact that 5 is prime;
- (Greater 5 3) represents the fact that 5 is greater than 3.
When a predicate is applied on all its arguments, it becomes a
proposition (that is, a formula which is either true or false).
Functions
In the same way, we would like to talk about functions.
Functions are different from predicates in the sense that they take objects
and return objects. An example of function is the sum of two numbers.
As for predicates, we use the applicative notation to represent functions:
- (Plus 5 3) represents the sum of 5 and 3.
Note that there is no difference between (Plus 5 3) and 8,
as they are only two different ways of expressing the same object.
The characteristic of 8 is that of being the simplest form,
i.e. the so-called normal form.
Variables
In our examples, we have used the notion of constant without saying
it: 5 and 8 are constants and represent two objects of
type integer number. In addition to constants, we have variables.
For variables, we normally use the following names:
x, y, z....
For example, (Greater (Plus x y) x) represents the fact that
the sum of object x and object y is greater than
object x.
To variables is associated the notion of substitution that
allows to replace a variable with an expression:
F[x <- E] means that inside the formula F,
every occurrence of variable x is replaced by expression E.
If F is the previous formula, we have that
F[x <- (Plus 3 z)] gives
(Greater (Plus (Plus 3 z) y) (Plus 3 z)).
Quantifiers
Universal quantifier
The universal quantifier allows us to build formulae that are true for
all objects.
For example, ∀x. (P x x) represents the fact that for every
object x, x is in relation with itself through predicate
P, meaning that P is a reflexive relation.
Existential quantifier
The existential quantifier allows us to build formulae that are true
for at least one object.
For example, ∀n. ∃p. (Greater p n) ∧ (Prime p)
expresses the fact that for every number n there exists a number
p such that p is greater than n and p
is a prime number, meaning that the set of prime numbers is infinite.
Free variable and bound variable
A variable is bound if it is under a quantifier with the same name
(the occurrence of the variable close to the quantifier is called
binding variable).
If this is not the case, the variable is free.
For example, in the formula ∃x. (P x y), x is bound
and y is free. The occurrence of x in ∃x
is binding.
A variable is bound to the closest quantifier.
For example, in the formula ∃x. ∀x. (P x)
the occurrence of variable x inside (P x) is bound to the
universal quantifier.
The name of bound variables is not significative:
∀x. ∃y. (P x y) is equivalent to
∀z. ∃t. (P z t) (renaming of binding and bound variables).
Substitutions respect quantifiers.
For example, ((P x) ∧ (∀x. (Q x x)))[x <- a] gives
((P a) ∧ (∀x. (Q x x))).
Implementation
For the implementation of bound variables, one usually uses deBruijn indices.
A bound variable is represented by a natural number that denotes how many
quantifiers one needs to cross in the tree-data structure of the formula in
order to reach the quantifier that binds that variable.
For example, the formula ∀n. ∃p. (Greater p n) ∧
(Prime p) is represented as (FORALL (EX (AND (Greater (VAR 0) (VAR 1)) (Prime (VAR 0))))).
Exercises
F1.Write the formula that represents the fact
that the predicate P is symmetric.
F2. Write the formula that represents the fact
that the predicate P is transitive.
F3. Write the formula that represents the fact
that a function f with one parameter is injective.
One can assume the existence of an equality predicate, written x=y.
F4. Write the formula that represents the fact
that a function f with one parameter is surjective.
Monica Nesi