Logic for Computer Scientists/Predicate Logic/Syntax

< Logic for Computer Scientists‎ | Predicate Logic



Definition 1 (Syntax of predicate logic - Terms)Edit

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)Edit

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_1, x_2 and x_3, 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: Bound and Free Occurrences of VariablesEdit

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)))