Logic for Computer Scientists/Predicate Logic/Syntax

Definition 1 (Syntax of predicate logic - Terms)

Assume a

• countable set of function symbols $\{ f{_i}^k \mid i,k =1,2,3,\cdots \}$
• a countable set of $\{ x_i \mid i = 1,2,3, \cdots\}$

The set of terms is defined by the following induction:

• Variables x_i are terms.
• If $t_1, \cdots, t_k$ are terms and $f_i^k$ is a function symbol, then $f_i^k(t_1, \cdots, t_k)$ is a term.

Terms of type $f_i^0()$ are special ones, they are called constants. In this case we omit the braces and denote them as $f_i^0$.

Terms are the syntactic counterpart of the above mentioned objects. Constants will denote the elements of the domain and function symbols will denote a way to refer to such objects.

The following definition introduces the formulae.

Definition 2 (Syntax of predicate logic - Formulae)

Assume a countable set of predicate symbols$\{ p_i^k \mid i = 1,2,3, \cdots\}$. The set of (well-formed) formulae is defined by the following induction:

• If $t_1,\cdots, t_k$ are terms and $P_i^k$ is a predicate symbol, then $P_i^k(t_1, \cdots, t_k)$ is a formula.
• If F and G are formulae, then $(F\land G)$ and $(F\lor G)$ are formulae.
• If F is a formula, then $\lnot F$ is a formula.
• If x is a variable and F a formula, then $\forall x F$ and $\exists x F$ are formulae.

Formulae of type $P_i^k(t_1, \cdots, t_k)$ are called atoms or atomic formulae.

Note that the concept of subformulae applies exactly like in the propositional case (Syntax (Propositional Logic)).

We introduce the following abbreviations, which will be used with indices as well:

u,v,w,x,z,			for variables
$a,b,c, \cdots$			for constants
$f,g,h, \cdots$			for function symbols
$p,q,r, \cdots$			for predicate symbols

Note the the arity of function and predicate symbols is ommited in these abbreviations; we assume that it will be obvious from the context.

Example: Assume we want to represent the following equation, which holds for arbitrary elements in a field:

x * (y + z) = x * y + x * z

The two operators * and + are represented in a predicate logic formula as binary function symbols $f_1^2$ and $f_2^2$, the three variables are x₁,x₂ and x₃, and the equality relation = is the binary predicate symbol $P_1^2$. Altogether we have the following formula in predicate logic:

$\forall x_1 \forall x_2 \forall x_3 (P_1^2(f_2^2(x_1, f_1^2(x_2,x_3)), f_1^2(f_2^2(x_1,x_2), f_2^2(x_1,x_3))))$

In the following we will use the obvious and more liberal notation as in the propositional case.

Definition 3

An occurrence of a variable x in a formula F is called bound, if it occurs in a subformula of F which is of the form $\exists x \;G$ or $\forall x\;G$. Otherwise we call the occurrence free.

A formula, which does not contain a free occurrence of a variable is called closed.

Example: The following formula contains both free and bound occurrences of x and y.

$\forall z(Q(z) \land \forall x(P(x,y)) \lor \exists y(P(x, y)))$